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 holds
for b being Real st b >= c holds
( f is_+infty_improper_integrable_on b & improper_integral_+infty (f,b) = +infty )
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 implies for b being Real st b >= c holds
( f is_+infty_improper_integrable_on b & improper_integral_+infty (f,b) = +infty ) )
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 ; :: thesis: for b being Real st b >= c holds
( f is_+infty_improper_integrable_on b & improper_integral_+infty (f,b) = +infty )
let b be Real; :: thesis: ( b >= c implies ( f is_+infty_improper_integrable_on b & improper_integral_+infty (f,b) = +infty ) )
assume A4: b >= c ; :: thesis: ( f is_+infty_improper_integrable_on b & improper_integral_+infty (f,b) = +infty )
consider I being PartFunc of REAL,REAL such that
A5: dom I = [.c,+infty.[ 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;
improper_integral_+infty (f,c) <> infty_ext_right_integral (f,c) by A3;
then A8: not f is_+infty_ext_Riemann_integrable_on c by A2, Th27;
+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 H₁( Element of LB) -> Element of REAL = In ((integral (f,b,$1)),REAL);
consider Intf being Function of LB,REAL such that
A9: for x being Element of LB holds Intf . x = H₁(x) from FUNCT_2:sch 4();
A10: dom Intf = LB by FUNCT_2:def 1;
then reconsider Intf = Intf as PartFunc of REAL,REAL by RELSET_1:5;
A11: 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 A9, A10;
hence Intf . x = integral (f,b,x) ; :: thesis: verum

end;

A12: 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
A13: ( g > max (b,r) & g in dom I ) by A8, A3, A2, A5, Def4, INTEGR10:def 5, LIMFUNC1:46;
A14: ( max (b,r) >= b & max (b,r) >= r ) by XXREAL_0:25;
then A15: ( g > b & g > r ) by A13, XXREAL_0:2;
g in dom Intf by A10, A14, A13, XXREAL_0:2, XXREAL_1:236;
hence ex g being Real st
( g > r & g in dom Intf ) by A15; :: thesis: verum

end;

A16: for g1 being Real ex r being Real st
for r1 being Real st r1 > r & r1 in dom Intf holds
g1 < Intf . r1

proof

let g1 be Real; :: thesis: ex r being Real st
for r1 being Real st r1 > r & r1 in dom Intf holds
g1 < Intf . r1
consider r being Real such that
A17: for r1 being Real st r1 > r & r1 in dom I holds
g1 + (integral (f,c,b)) < I . r1 by A8, A7, A3, A2, A5, A6, Def4, INTEGR10:def 5, LIMFUNC1:46;
set R = max (b,r);
take max (b,r) ; :: thesis: for r1 being Real st r1 > max (b,r) & r1 in dom Intf holds
g1 < Intf . r1
thus for r1 being Real st r1 > max (b,r) & r1 in dom Intf holds
g1 < Intf . r1 :: thesis: verum

proof

let r1 be Real; :: thesis: ( r1 > max (b,r) & r1 in dom Intf implies g1 < Intf . r1 )
assume A18: ( r1 > max (b,r) & r1 in dom Intf ) ; :: thesis: g1 < Intf . r1
( max (b,r) >= b & max (b,r) >= r ) by XXREAL_0:25;
then A19: ( r1 > b & r1 > r ) by A18, XXREAL_0:2;
then A20: r1 > c by A4, XXREAL_0:2;
r1 in dom I by A19, A5, A4, XXREAL_0:2, XXREAL_1:236;
then g1 + (integral (f,c,b)) < I . r1 by A17, A19;
then A21: g1 + (integral (f,c,b)) < integral (f,c,r1) by A6, A20, A5, XXREAL_1:236;
A22: ( f is_integrable_on ['c,r1'] & f | ['c,r1'] is bounded ) by A20, A2;
A23: ['c,r1'] = [.c,r1.] by A19, A4, XXREAL_0:2, INTEGRA5:def 3;
then ['c,r1'] c= [.c,+infty.[ by XXREAL_1:251;
then A24: ['c,r1'] c= dom f by A1;
b in ['c,r1'] by A23, A19, A4, XXREAL_1:1;
then integral (f,c,r1) = (integral (f,b,r1)) + (integral (f,c,b)) by A20, A22, A24, INTEGRA6:17;
then g1 < integral (f,b,r1) by A21, XREAL_1:6;
hence g1 < Intf . r1 by A11, A18; :: thesis: verum

end;

end;

hence A25: f is_+infty_improper_integrable_on b by A10, A11, A1, A2, A4, Lm10, A12, LIMFUNC1:46; :: thesis: improper_integral_+infty (f,b) = +infty
Intf is divergent_in+infty_to+infty by A12, A16, LIMFUNC1:46;
hence improper_integral_+infty (f,b) = +infty by A10, A11, A25, Def4; :: thesis: verum