theorem Th21: :: INTEGR24:21

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