+ Lemma RestrictToImage_splits_niso : F ≃ (RestrictToImage >>>> FullImage_InclusionFunctor).
+ unfold IsomorphicFunctors.
+ exists (fun A => iso_id (fobj A)).
+ intros.
+ simpl.
+ setoid_rewrite left_identity.
+ setoid_rewrite right_identity.
+ reflexivity.
+ Qed.
+