proposition: Lemma Vf_image_P x: sub x (source f) -> forall y, (inc y (Vfs f x) <-> exists2 u, inc u x & y = Vf f u).
proof: Proof. rewrite /Vfs => ss;split. by move/dirim_P => [a ax Jg]; ex_tac; apply: Vf_pr. move=> [u ux ->]; apply/dirim_P; ex_tac;apply: Vf_pr3; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)