proposition: Lemma inverse_image_indexed_union : forall {A X Y:Type} (f:X->Y) (F:IndexedFamily A Y), inverse_image f (IndexedUnion F) = IndexedUnion (fun a:A => inverse_image f (F a)).
proof: Proof. intros. apply Extensionality_Ensembles; split; red; intros. - destruct H. inversion_clear H. exists a. constructor. exact H0. - destruct H. inversion_clear H. constructor. exists a. exact H0. Qed.
imports: FunctionProperties Ensembles EnsemblesImplicit EnsemblesSpec IndexedFamilies