proposition: Lemma Im_singleton {X Y : Type} (f : X -> Y) (x : X) : Im (Singleton x) f = Singleton (f x).
proof: Proof. apply Extensionality_Ensembles; split. - intros y Hy. destruct Hy as [x0 Hx0]; subst. destruct Hx0; constructor. - intros y Hy. destruct Hy. apply Im_def. constructor. Qed.
imports: ZornsLemma(EnsemblesImplicit) ZornsLemma(FunctionProperties)