proposition: Lemma exercise4_2a g x: direct_image g x = range (g \cap (x \times (range g))).
proof: Proof. set_extens y. move /dirim_P => [a ax pg]; apply/funI_P; exists (J a y); aw;trivial. apply /setI2_P; split => //; apply:setXp_i => //; ex_tac. move /funI_P => [a /setI2_P [pg /setX_P [pa pb pc]] ->]. by apply/dirim_P; ex_tac; rewrite pa. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)