proposition: Lemma image_surjective_ens_range {X Y : Type} (f : X -> Y) (U : Ensemble X) (V : Ensemble Y) : range f U V -> surjective_ens f U V -> V = Im U f.
proof: Proof. intros Hf0 Hf1. apply Extensionality_Ensembles; split. - intros y Hy. specialize (Hf1 y Hy) as [x [Hx Hxy]]; subst. apply Im_def. assumption. - intros y Hy. destruct Hy as [x Hx y Hy]. subst. apply Hf0. assumption. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(DecidableDec EnsemblesImplicit Families FunctionProperties Image InverseImage Powerset_facts Proj1SigInjective) Coq(RelationClasses)