diff --git a/Lebesgue/Subset_system_base.v b/Lebesgue/Subset_system_base.v
index c6e45c9932f457a68d06dc4723ccfaffdb61c993..8d9ec662b1e5007571ec5d1e80b2083a5610034d 100644
--- a/Lebesgue/Subset_system_base.v
+++ b/Lebesgue/Subset_system_base.v
@@ -195,7 +195,7 @@ Variable P1 : (U1 -> Prop) -> Prop. (* Subset system. *)
 Variable P2 : (U2 -> Prop) -> Prop. (* Subset system. *)
 
 (* From Lemma 524 p. 93 (v2) *)
-Definition Image : (U2 -> Prop) -> Prop := fun A2 => P1 (preimage f A2).
+Definition Image : (U2 -> Prop) -> Prop := preimage (preimage f) P1.
 
 (* From Lemma 523 p. 93 (v2) *)
 Definition Preimage : (U1 -> Prop) -> Prop := image (preimage f) P2.
@@ -518,11 +518,19 @@ Variable f23 : U2 -> U3.
 Lemma Image_compose :
   forall P1, Image (compose f23 f12) P1 = Image f23 (Image f12 P1).
 Proof.
-Admitted.
+intros; unfold Image; subset_unfold; easy.
+Qed.
 
 Lemma Preimage_compose :
   forall P3, Preimage (compose f23 f12) P3 = Preimage f12 (Preimage f23 P3).
 Proof.
+intros P3; unfold Preimage; subset_ext_auto A1 HA1.
+induction HA1 as [A3 HA3].
+admit.
+
+induction HA1 as [A2 HA2].
+
+
 Admitted.
 
 End Image_Preimage_Facts2.