theorem Th84: :: MESFUN15:82

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 & abs f is_+infty_ext_Riemann_integrable_on a holds
( f | A is_integrable_on L-Meas & improper_integral_+infty (f,a) = Integral (L-Meas,(f | A)) )