proposition: Lemma Exercise4_6i E F A: E46b_hyp E F A -> E46b_conc E A.
proof: Proof. move=> [f [injf sf tf] fp] H HE. have ff: function f by fct_tac. have shs:sub H (source f) by ue. have pa:sub (Vfs f H) (union (fun_image H A)). move=> t /(Vf_image_P ff shs) [u uH ->]. move: (fp _ (HE _ uH)) => aux; apply /setU_P;exists (A u) => //. apply /funI_P; ex_tac. move: (sub_smaller pa) => pb. move: (Eq_restriction1 shs injf). by move /card_eqP => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)