let f be PartFunc of REAL,REAL; :: thesis: for c being Real st right_closed_halfline c c= dom f & f is_+infty_improper_integrable_on c & improper_integral_+infty (f,c) = infty_ext_right_integral (f,c) holds
for b being Real st b >= c holds
( f is_+infty_improper_integrable_on b & improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) )
let c be Real; :: thesis: ( right_closed_halfline c c= dom f & f is_+infty_improper_integrable_on c & improper_integral_+infty (f,c) = infty_ext_right_integral (f,c) implies for b being Real st b >= c holds
( f is_+infty_improper_integrable_on b & improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) ) )
assume that
A1: right_closed_halfline c c= dom f and
A2: f is_+infty_improper_integrable_on c and
A3: improper_integral_+infty (f,c) = infty_ext_right_integral (f,c) ; :: thesis: for b being Real st b >= c holds
( f is_+infty_improper_integrable_on b & improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) )
let b be Real; :: thesis: ( b >= c implies ( f is_+infty_improper_integrable_on b & improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) ) )
assume A4: b >= c ; :: thesis: ( f is_+infty_improper_integrable_on b & improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) )
consider I being PartFunc of REAL,REAL such that
A5: dom I = right_closed_halfline c and
A6: for x being Real st x in dom I holds
I . x = integral (f,c,x) and
A7: ( I is convergent_in+infty or I is divergent_in+infty_to+infty or I is divergent_in+infty_to-infty ) by A2;
A8: now :: thesis: not I is divergent_in+infty_to+infty
assume I is divergent_in+infty_to+infty ; :: thesis: contradiction
then not f is_+infty_ext_Riemann_integrable_on c by A5, A6, Th28;
hence contradiction by A2, A3, Th27; :: thesis: verum
end;
A9: now :: thesis: not I is divergent_in+infty_to-infty
assume I is divergent_in+infty_to-infty ; :: thesis: contradiction
then not f is_+infty_ext_Riemann_integrable_on c by A5, A6, Th28;
hence contradiction by A2, A3, Th27; :: thesis: verum
end;
+infty > b by XREAL_0:def 1, XXREAL_0:9;
then reconsider LB = [.b,+infty.[ as non empty Subset of REAL by XXREAL_1:3;
deffunc H1( Element of LB) -> Element of REAL = In ((integral (f,b,$1)),REAL);
consider Intf being Function of LB,REAL such that
A10: for x being Element of LB holds Intf . x = H1(x) from FUNCT_2:sch 4();
 A11: dom Intf = LB by FUNCT_2:def 1;
then reconsider Intf = Intf as PartFunc of REAL,REAL by RELSET_1:5;
A12: for x being Real st x in dom Intf holds
Intf . x = integral (f,b,x)
proof
let x be Real; :: thesis: ( x in dom Intf implies Intf . x = integral (f,b,x) )
assume x in dom Intf ; :: thesis: Intf . x = integral (f,b,x)
then Intf . x = In ((integral (f,b,x)),REAL) by A10, A11;
hence Intf . x = integral (f,b,x) ; :: thesis: verum
end;
A13: for r being Real ex g being Real st
( g > r & g in dom Intf )
proof
let r be Real; :: thesis: ex g being Real st
( g > r & g in dom Intf )
set R = max (b,r);
consider g being Real such that
A14: ( g > max (b,r) & g in dom I ) by A7, A8, A9, LIMFUNC1:44;
A15: ( max (b,r) >= b & max (b,r) >= r ) by XXREAL_0:25;
then A16: ( g > b & g > r ) by A14, XXREAL_0:2;
g in [.b,+infty.[ by A15, A14, XXREAL_0:2, XXREAL_1:236;
hence ex g being Real st
( g > r & g in dom Intf ) by A11, A16; :: thesis: verum
end;
consider g being Real such that
A17: for g1 being Real st 0 < g1 holds
ex r being Real st
for r1 being Real st r1 > r & r1 in dom I holds
|.((I . r1) - g).| < g1 by A7, A8, A9, LIMFUNC1:44;
set G = g - (integral (f,c,b));
A18: for g1 being Real st 0 < g1 holds
ex r being Real st
for r1 being Real st r1 > r & r1 in dom Intf holds
|.((Intf . r1) - (g - (integral (f,c,b)))).| < g1
proof
let g1 be Real; :: thesis: ( 0 < g1 implies ex r being Real st
for r1 being Real st r1 > r & r1 in dom Intf holds
|.((Intf . r1) - (g - (integral (f,c,b)))).| < g1 )
assume 0 < g1 ; :: thesis: ex r being Real st
for r1 being Real st r1 > r & r1 in dom Intf holds
|.((Intf . r1) - (g - (integral (f,c,b)))).| < g1
then consider r being Real such that
A19: for r1 being Real st r1 > r & r1 in dom I holds
|.((I . r1) - g).| < g1 by A17;
set R = max (b,r);
for r1 being Real st r1 > max (b,r) & r1 in dom Intf holds
|.((Intf . r1) - (g - (integral (f,c,b)))).| < g1
proof
let r1 be Real; :: thesis: ( r1 > max (b,r) & r1 in dom Intf implies |.((Intf . r1) - (g - (integral (f,c,b)))).| < g1 )
assume that
A20: r1 > max (b,r) and
A21: r1 in dom Intf ; :: thesis: |.((Intf . r1) - (g - (integral (f,c,b)))).| < g1
( max (b,r) >= r & max (b,r) >= b ) by XXREAL_0:25;
then A22: ( r1 > r & r1 > b ) by A20, XXREAL_0:2;
A23: dom Intf c= dom I by A4, A5, A11, XXREAL_1:38;
then A24: |.((I . r1) - g).| < g1 by A22, A19, A21;
A25: r1 >= c by A5, A21, A23, XXREAL_1:3;
then A26: ( f is_integrable_on ['c,r1'] & f | ['c,r1'] is bounded ) by A2;
A27: [.c,r1.] = ['c,r1'] by A25, INTEGRA5:def 3;
then ['c,r1'] c= [.c,+infty.[ by XXREAL_1:251;
then A28: ['c,r1'] c= dom f by A1;
A29: b in ['c,r1'] by A22, A4, A27, XXREAL_1:1;
(I . r1) - g = (integral (f,c,r1)) - g by A6, A21, A23
.= ((integral (f,b,r1)) + (integral (f,c,b))) - g by A25, A26, A28, A29, INTEGRA6:17
.= (integral (f,b,r1)) - (g - (integral (f,c,b))) ;
hence |.((Intf . r1) - (g - (integral (f,c,b)))).| < g1 by A21, A24, A12; :: thesis: verum
end;
hence ex r being Real st
for r1 being Real st r1 > r & r1 in dom Intf holds
|.((Intf . r1) - (g - (integral (f,c,b)))).| < g1 ; :: thesis: verum
end;
hence A30: f is_+infty_improper_integrable_on b by A11, A12, A13, A1, A2, A4, Lm10, LIMFUNC1:44; :: thesis: improper_integral_+infty (f,b) = infty_ext_right_integral (f,b)
then f is_+infty_ext_Riemann_integrable_on b by A11, A12, A13, A18, LIMFUNC1:44, INTEGR10:def 5;
hence improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) by A30, Th27; :: thesis: verum