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