theorem Th54: :: MESFUN15:52

for f being PartFunc of REAL,REAL
for a being Real
for A being non empty Subset of REAL st dom f = REAL & f is_improper_integrable_on_REAL & f is nonnegative holds
( improper_integral_on_REAL f = Integral (L-Meas,f) & ( f is infty_ext_Riemann_integrable implies f is_integrable_on L-Meas ) & ( not f is infty_ext_Riemann_integrable implies Integral (L-Meas,f) = +infty ) )