proposition: Lemma image_as_Im {A B : Type} (U : Ensemble A) (f : A -> B) : image U f = Im U f.
proof: Proof. apply Extensionality_Ensembles; split; intros y Hy. - destruct Hy as [x [Hx Hy]]. subst. exists x; auto. - inversion Hy; subst; clear Hy. exists x; auto. Qed.
imports: Coq(ClassicalDescription Ensembles Image ProofIrrelevance) ZornsLemma(EnsemblesImplicit FunctionProperties ImageImplicit) hydras(MoreEpsilonIota)