theorem Th16: :: INTEGR25:16

for f being PartFunc of REAL,REAL
for a being Real st right_closed_halfline a c= dom f & f is_+infty_ext_Riemann_integrable_on a holds
for b being Real st a <= b holds
f is_+infty_ext_Riemann_integrable_on b