theorem Th83: :: MESFUN15:81

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