proposition: Lemma EnsembleProduct_Union_dist {X Y : Type} (U : Ensemble X) (V0 V1 : Ensemble Y) : Union (EnsembleProduct U V0) (EnsembleProduct U V1) = EnsembleProduct U (Union V0 V1).
proof: Proof. apply Extensionality_Ensembles; split; red; intros. - destruct H. + destruct H. split; try assumption. left. assumption. + destruct H. split; try assumption. right. assumption. - destruct H. inversion H0; subst; clear H0. + left. split; assumption. + right. split; assumption. Qed.
imports: ZornsLemma(EnsemblesImplicit InverseImage)