proposition: Lemma inverse_image_composition: forall {X Y Z:Type} (f:Y->Z) (g:X->Y) (U:Ensemble Z), inverse_image (fun x:X => f (g x)) U = inverse_image g (inverse_image f U).
proof: Proof. intros. apply Extensionality_Ensembles; split; red; intros. - constructor; constructor. destruct H. assumption. - destruct H; inversion H. constructor; trivial. Qed.
imports: ZornsLemma(IndexedFamilies Powerset_facts)