proposition: Lemma Im_compose {X Y Z : Type} (f : X -> Y) (g : Y -> Z) (U : Ensemble X) : Im U (compose g f) = Im (Im U f) g.
proof: Proof. apply Extensionality_Ensembles; split. - intros z Hz. destruct Hz as [x Hx z Hz]. subst. unfold compose. do 2 apply Im_def. assumption. - intros z Hz. destruct Hz as [y Hy z Hz]. subst. destruct Hy as [x Hx y Hy]. subst. unfold compose. exists x; auto. Qed.
imports: ZornsLemma(EnsemblesImplicit) ZornsLemma(FunctionProperties)