theorem :: MESFUN15:83

for f being PartFunc of REAL,REAL st dom f = REAL & f is_improper_integrable_on_REAL & abs f is infty_ext_Riemann_integrable holds
( f is_integrable_on L-Meas & improper_integral_on_REAL f = Integral (L-Meas,f) )