theorem Th18: :: INTEGR25:18

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