proposition: Lemma EnsembleProduct_Empty_l {X Y : Type} V : @EnsembleProduct X Y Empty_set V = Empty_set.
proof: Proof. apply Extensionality_Ensembles; split; red; intros. - destruct x. destruct H. destruct H. - destruct H. Qed.
imports: ZornsLemma(EnsemblesImplicit InverseImage)