proposition: Lemma inverse_image_union2 {X Y : Type} (f : X -> Y) (U V : Ensemble Y) : inverse_image f (Union U V) = Union (inverse_image f U) (inverse_image f V).
proof: Proof. apply Extensionality_Ensembles. split; red; intros. - destruct H. inversion H; subst; [ left | right ]; now constructor. - now inversion H; destruct H0; subst; constructor; [ left | right ]. Qed.
imports: FunctionProperties Ensembles EnsemblesImplicit EnsemblesSpec IndexedFamilies