theorem Th49: :: MESFUN15:47

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