proposition: Lemma exercise4_2b g x: direct_image g x = direct_image g (x \cap (domain g)).
proof: Proof. set_extens t; move /dirim_P => [y ys Jg]; apply/dirim_P. ex_tac; apply /setI2_P; split=> //; ex_tac. move /setI2_P: ys => [pa pb]; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)