Only keep _fun versions, and skip the suffix.

Lebesgue/Set_theory/Set_fun.v

@@ -148,30 +148,17 @@ Proof.
 easy.
 Qed.
 
-Lemma image_compose_fun :
-  image (compose f32 f21) = fun A1 => image f32 (image f21 A1).
-Proof.
-apply fun_ext; intros A1; apply set_ext_equiv; split; intros x3 Hx3.
-induction Hx3 as [x1 Hx1]; easy.
-induction Hx3 as [x2 Hx2], Hx2 as [x1 Hx1].
-replace (f32 (f21 x1)) with (compose f32 f21 x1); easy.
-Qed.
-
 Lemma image_compose :
-  forall A1, image (compose f32 f21) A1 = image f32 (image f21 A1).
+  image (compose f32 f21) = compose (image f32) (image f21).
 Proof.
-rewrite image_compose_fun; easy.
+apply fun_ext; intros A1; apply set_ext_equiv; split; intros x3.
+intros [x1 Hx1]; easy.
+intros [x2 [x1 Hx1]]; rewrite <- compose_eq; easy.
 Qed.
 
 (* Useful? *)
-Lemma preimage_compose_fun :
-  preimage (compose f32 f21) = fun A3 => preimage f21 (preimage f32 A3).
-Proof.
-easy.
-Qed.
-
 Lemma preimage_compose :
-  forall A3, preimage (compose f32 f21) A3 = preimage f21 (preimage f32 A3).
+  preimage (compose f32 f21) = compose (preimage f21) (preimage f32).
 Proof.
 easy.
 Qed.