diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index b7c04b703d..dc8fdf7201 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -146,6 +146,9 @@
   + `sedDI_closedP` -> `setD_closedP`
   + `setringDI` -> `setringD`
 
+- in `lebesgue_integral.v`:
+  + `Rintegral_setU_EFin` -> `Rintegral_setU`
+
 ### Generalized
 
 - in `sequences.v`,
diff --git a/theories/ftc.v b/theories/ftc.v
index 1210e60f14..d75df24299 100644
--- a/theories/ftc.v
+++ b/theories/ftc.v
@@ -560,7 +560,7 @@ have [d [d0 /= {}int_normr_cont]] := int_normr_cont _ e0.
 near=> x.
 rewrite [in X in X - _](@itv_bndbnd_setU _ _ _ (BRight x))//;
   [|by rewrite bnd_simp ltW..].
-rewrite Rintegral_setU_EFin//=; last 2 first.
+rewrite Rintegral_setU//=; last 2 first.
   rewrite -itv_bndbnd_setU// ?bnd_simp; last 2 first.
     by near: x; exact: nbhs_left_ge.
     exact/ltW.
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index d851f410de..351b1512be 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.v
@@ -4730,7 +4730,7 @@ by apply: ge0_le_integral => //=; do 2 apply: measurableT_comp => //;
   exact/measurable_EFinP.
 Qed.
 
-Lemma Rintegral_setU_EFin (A B : set T) (f : T -> R) :
+Lemma Rintegral_setU (A B : set T) (f : T -> R) :
     d.-measurable A -> d.-measurable B ->
     mu.-integrable (A `|` B) (EFin \o f) -> [disjoint A & B] ->
   \int[mu]_(x in (A `|` B)) f x = \int[mu]_(x in A) f x + \int[mu]_(x in B) f x.
@@ -4787,6 +4787,8 @@ by rewrite /Rintegral integralB_EFin// fineB//; exact: integral_fune_fin_num.
 Qed.
 
 End Rintegral.
+#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `Rintegral_setU`")]
+Notation Rintegral_setU_EFin := Rintegral_setU (only parsing).
 
 Section ae_ge0_le_integral.
 Local Open Scope ereal_scope.
@@ -6938,7 +6940,7 @@ move=> itf; rewrite le_eqVlt => /predU1P[ax|ax xb].
 rewrite (@itv_bndbnd_setU _ _ _ (BLeft x)); last 2 first.
   by case: a ax {itf} => -[].
   by rewrite (le_trans _ xb)// bnd_simp.
-rewrite Rintegral_setU_EFin//=.
+rewrite Rintegral_setU//=.
 - rewrite addrAC Rintegral_itv_bndo_bndc//; last first.
     apply: integrableS itf => //; apply: subset_itvl.
     by rewrite (le_trans _ xb)// bnd_simp.