theorem Th21: :: INTEGR25:21

for f being PartFunc of REAL,REAL
for a being Real st f is_+infty_ext_Riemann_integrable_on a holds
f is_+infty_improper_integrable_on a