let f, Intf be PartFunc of REAL,REAL; for b being Real st f is_-infty_improper_integrable_on b & dom Intf = left_closed_halfline b & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) ) & Intf is convergent_in-infty holds
improper_integral_-infty (f,b) = lim_in-infty Intf
let b be Real; ( f is_-infty_improper_integrable_on b & dom Intf = left_closed_halfline b & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) ) & 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 = left_closed_halfline b
and
A3:
for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b)
and
A4:
Intf is convergent_in-infty
; 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 6;
then A6:
improper_integral_-infty (f,b) = infty_ext_left_integral (f,b)
by A1, Th22;
consider I being PartFunc of REAL,REAL such that
A7:
dom I = left_closed_halfline b
and
A8:
for x being Real st x in dom I holds
I . x = integral (f,x,b)
and
I is convergent_in-infty
and
A9:
infty_ext_left_integral (f,b) = lim_in-infty I
by A5, INTEGR10:def 8;
hence
improper_integral_-infty (f,b) = lim_in-infty Intf
by A6, A9, A2, A7, PARTFUN1:5; verum