proposition: Lemma iim_fun_r f (h:=restriction_to_image f): function f -> forall a, Vfs f a = Vfi (inverse_fun h) a.
proof: Proof. move => ff a. have aux:=(proj1 (function_fgraph (proj1 (restriction_to_image_fs ff)))). rewrite /Vfi/Vfs /inverse_image. rewrite corresp_g (igraph_involutive aux) corresp_g. congr (direct_image _ a); symmetry;apply/setI2id_Pl. exact:(proj2 (proj31 ff)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)