proposition: Lemma Exercise4_6j E F A G: E46c_hyp E F A G -> (E46b_conc E A /\ E46c_conc E A G).
proof: Proof. move => [f [[injf pa pb] pc pd]]. split; first by apply: (@Exercise4_6i _ F) ; exists f => //. move => L LG; set K := Vfi f L. have ff: function f by fct_tac. have Ksf: sub K (source f). move=> t /iim_graph_P [u uL Jg]; Wtac. have aux: L = Vfs f K. set_extens t. move => tL; apply /(Vf_image_P ff Ksf). move: (pc _ (LG _ tL)) => /(Imf_P ff) [x xsf Jg]. exists x => //; apply /iim_graph_P; exists t => //; rewrite Jg; Wtac. move /(Vf_image_P ff Ksf) => [u ui ->]; move:ui => /iim_graph_P [v vL Jg]. by rewrite - (Vf_pr ff Jg). move: (Eq_restriction1 Ksf injf). rewrite -aux; move /card_eqP=> <-; apply: sub_smaller. move => t /iim_graph_P [u uL jg]; move: (p1graph_source ff jg) => tf. rewrite pa in tf;apply: Zo_i => //; move: (pd _ tf); rewrite - (Vf_pr ff jg). by move=> ua; exists u; apply /setI2_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)