theorem Th48: :: MESFUN15:46

for f being PartFunc of REAL,REAL
for b being Real
for A being non empty Subset of REAL st left_closed_halfline b c= dom f & A = left_closed_halfline b & f is_-infty_improper_integrable_on b & f is nonpositive holds
( improper_integral_-infty (f,b) = Integral (L-Meas,(f | A)) & ( f is_-infty_ext_Riemann_integrable_on b implies f | A is_integrable_on L-Meas ) & ( not f is_-infty_ext_Riemann_integrable_on b implies Integral (L-Meas,(f | A)) = -infty ) )