proposition: Lemma surjective_ens_Im {X Y : Type} (f : X -> Y) (U : Ensemble X) : surjective_ens f U (Im U f).
proof: Proof. intros y Hy. inversion Hy; subst; clear Hy. exists x; split; auto. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(DecidableDec EnsemblesImplicit Families FunctionProperties Image InverseImage Powerset_facts Proj1SigInjective) Coq(RelationClasses)