diff --git a/Lebesgue/Set_theory/Set_base.v b/Lebesgue/Set_theory/Set_base.v
index c22db4cacde4338b5ab9490c71c3b6273848e4c5..e4d81173b3c5ad802c1fc93b597339cc1a5df60d 100644
--- a/Lebesgue/Set_theory/Set_base.v
+++ b/Lebesgue/Set_theory/Set_base.v
@@ -2491,9 +2491,9 @@ Variable f : U1 -> U2.
 
 (** Facts about image. *)
 
-Lemma image_id : forall {U : Type} (A : set U), image id A = A.
+Lemma image_id : forall {U : Type}, @image U U id = id.
 Proof.
-intros; apply set_ext_equiv; split; intros x Hx.
+intros; apply fun_ext; intros A; apply set_ext_equiv; split; intros x Hx.
 induction Hx as [x Hx]; easy.
 rewrite <- id_eq; easy.
 Qed.