let f, Intf be PartFunc of REAL,REAL; :: thesis: for b being Real st f is_+infty_improper_integrable_on b & dom Intf = right_closed_halfline b & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,b,x) ) & Intf is convergent_in+infty holds
improper_integral_+infty (f,b) = lim_in+infty Intf
let b be Real; :: thesis: ( f is_+infty_improper_integrable_on b & dom Intf = right_closed_halfline b & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,b,x) ) & Intf is convergent_in+infty implies improper_integral_+infty (f,b) = lim_in+infty Intf )
assume that
A1: f is_+infty_improper_integrable_on b and
A2: dom Intf = right_closed_halfline b and
A3: for x being Real st x in dom Intf holds
Intf . x = integral (f,b,x) and
A4: Intf is convergent_in+infty ; :: thesis: improper_integral_+infty (f,b) = lim_in+infty Intf
A5: f is_+infty_ext_Riemann_integrable_on b by A1, A2, A3, A4, INTEGR10:def 5;
then A6: improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) by A1, Th27;
consider I being PartFunc of REAL,REAL such that
A7: dom I = right_closed_halfline b and
A8: for x being Real st x in dom I holds
I . x = integral (f,b,x) and
I is convergent_in+infty and
A9: infty_ext_right_integral (f,b) = lim_in+infty I by A5, INTEGR10:def 7;
now :: thesis: for x being Element of REAL st x in dom Intf holds
Intf . x = I . x
let x be Element of REAL ; :: thesis: ( x in dom Intf implies Intf . x = I . x )
assume A10: x in dom Intf ; :: thesis: Intf . x = I . x
then Intf . x = integral (f,b,x) by A3;
hence Intf . x = I . x by A2, A7, A8, A10; :: thesis: verum
end;
hence improper_integral_+infty (f,b) = lim_in+infty Intf by A6, A9, A2, A7, PARTFUN1:5; :: thesis: verum