let f be PartFunc of REAL,REAL; :: thesis: 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 & f is nonnegative holds
( f | A is_integrable_on L-Meas & improper_integral_-infty (f,b) = Integral (L-Meas,(f | A)) )
let b be Real; :: thesis: 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 & f is nonnegative holds
( f | A is_integrable_on L-Meas & improper_integral_-infty (f,b) = Integral (L-Meas,(f | A)) )
let A be non empty Subset of REAL; :: thesis: ( 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 & f is nonnegative implies ( f | A is_integrable_on L-Meas & improper_integral_-infty (f,b) = Integral (L-Meas,(f | A)) ) )
assume that
A1: left_closed_halfline b c= dom f and
A2: A = left_closed_halfline b and
A3: f is_-infty_improper_integrable_on b and
A4: abs f is_-infty_ext_Riemann_integrable_on b and
A5: f is nonnegative ; :: thesis: ( f | A is_integrable_on L-Meas & improper_integral_-infty (f,b) = Integral (L-Meas,(f | A)) )
f is_-infty_ext_Riemann_integrable_on b by A1, A3, A4, Th60;
hence ( f | A is_integrable_on L-Meas & improper_integral_-infty (f,b) = Integral (L-Meas,(f | A)) ) by A1, A2, A3, A5, Th47; :: thesis: verum