proposition: Lemma fun_bijection_is_ZL_bijection {U V : Type} {A : Ensemble U} {B : Ensemble V} (g : U -> V) (g_bij : fun_bijection A B g) : FunctionProperties.bijective (fun_restr (fun_bijection_codomain g_bij)).
proof: Proof. destruct g_bij as [H0 H1 H2]. split. - intros [x0 Hx0] [x1 Hx1] Hx. apply subset_eq_compat. inversion Hx; subst; clear Hx. apply H2; auto. - intros [y Hy]. simpl. specialize (H1 y Hy) as [x [Hx0 Hx1]]. subst. exists (exist _ x Hx0). apply subset_eq_compat. reflexivity. Qed.
imports: Coq(ClassicalDescription Ensembles Image ProofIrrelevance) ZornsLemma(EnsemblesImplicit FunctionProperties ImageImplicit) hydras(MoreEpsilonIota)