proposition: Lemma fun_bijection_codomain {U V : Type} {A : Ensemble U} {B : Ensemble V} (g : U -> V) (g_bij : fun_bijection A B g) : fun_codomain A B g.
proof: Proof. destruct g_bij; assumption. Defined.
imports: Coq(ClassicalDescription Ensembles Image ProofIrrelevance) ZornsLemma(EnsemblesImplicit FunctionProperties ImageImplicit) hydras(MoreEpsilonIota)