proposition: Lemma inverse_image_image_surjective_locally {X Y} (f : X -> Y) (T : Ensemble Y) : (forall y, In T y -> exists x, f x = y) -> Im (inverse_image f T) f = T.
proof: Proof. intros. extensionality_ensembles_inv. - subst. assumption. - specialize (H _ H0) as [x0]. subst. apply Im_def. constructor. assumption. Qed.
imports: ZornsLemma(IndexedFamilies Powerset_facts)