proposition: Lemma dirimE f X: fgraph f -> sub X (domain f) -> direct_image f X = fun_image X (Vg f).
proof: Proof. move => sgf sxd; set_extens t. move /dirim_P => [x xX pf]; apply /funI_P. move: (pr2_V sgf pf); aw => ->; ex_tac. move /funI_P => [z sX ->]; apply /dirim_P; ex_tac; apply: fdomain_pr1 => //. by apply: sxd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)