theorem Th25: :: INTEGR24:25

for f being PartFunc of REAL,REAL
for a, b being Real st [.a,b.[ c= dom f & f is_right_ext_Riemann_integrable_on a,b holds
for c being Real st a <= c & c < b holds
( f is_right_ext_Riemann_integrable_on c,b & ext_right_integral (f,a,b) = (integral (f,a,c)) + (ext_right_integral (f,c,b)) )