proposition: Lemma inverse_image_image_surjective {X Y : Type} (f : X -> Y) (T : Ensemble Y) : surjective f -> Im (inverse_image f T) f = T.
proof: Proof. intro. apply Extensionality_Ensembles. split; red; intros. - inversion H0. subst. now destruct H1. - destruct (H x). subst. now repeat econstructor. Qed.
imports: FunctionProperties Ensembles EnsemblesImplicit EnsemblesSpec IndexedFamilies