proposition: Lemma image_indexed_union (X Y I : Type) (F : IndexedFamily I X) (f : X -> Y) : Im (IndexedUnion F) f = IndexedUnion (fun i => Im (F i) f).
proof: Proof. apply Extensionality_Ensembles; split; red; intros. - inversion H; subst; clear H. inversion H0; subst; clear H0. exists a. exists x0. all: auto. - inversion H; subst; clear H. inversion H0; subst; clear H0. exists x0; [|reflexivity]. exists a. assumption. Qed.
imports: ZornsLemma(EnsemblesImplicit FunctionProperties)