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