proposition: Lemma direct_image_exten f f' a: fgraph f -> fgraph f' -> (forall x, inc x a -> Vg f x = Vg f' x) -> sub a (domain f) -> sub a (domain f') -> direct_image f a = direct_image f' a.
proof: Proof. move=> fgf fgf' sVVg adf adf'. set_extens x; move /dirim_P => [u us Jg]; apply /dirim_P; ex_tac. move: (pr2_V fgf Jg); aw; move=> ->; rewrite (sVVg _ us). by apply: fdomain_pr1 =>//; apply: adf'. move: (pr2_V fgf' Jg); aw; move=> ->; rewrite -(sVVg _ us). by apply: fdomain_pr1 =>//; apply: adf. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)