proposition: Lemma inverse_image_fst {X Y : Type} (U : Ensemble X) : inverse_image fst U = EnsembleProduct U (@Full_set Y).
proof: Proof. apply Extensionality_Ensembles; split; red; intros. - do 2 red. destruct H. auto with sets. - destruct H. constructor. auto. Qed.
imports: ZornsLemma(EnsemblesImplicit InverseImage)