theorem Th61: :: MESFUN15:59

for f being PartFunc of REAL,REAL
for a being Real st right_closed_halfline a c= dom f & f is_+infty_improper_integrable_on a & abs f is_+infty_ext_Riemann_integrable_on a holds
( f is_+infty_ext_Riemann_integrable_on a & improper_integral_+infty (f,a) <= improper_integral_+infty ((abs f),a) & improper_integral_+infty ((abs f),a) < +infty )