proposition: Lemma Union_Im {X Y : Type} (f : X -> Y) (U V : Ensemble X) : Union (Im U f) (Im V f) = Im (Union U V) f.
proof: Proof. apply Extensionality_Ensembles; split; red; intros. - destruct H. all: inversion H; subst; clear H. all: apply Im_def. 1: left. 2: right. all: assumption. - inversion H; subst; clear H. destruct H0; [left|right]. all: apply Im_def. all: assumption. Qed.
imports: ZornsLemma(EnsemblesImplicit) ZornsLemma(FunctionProperties)