theorem Th60: :: MESFUN15:58

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