let f be PartFunc of REAL,REAL; :: thesis:
let a be Real; :: thesis:
assume that
A1: right_closed_halfline a c= dom f and
A2: f is_+infty_ext_Riemann_integrable_on a ; :: thesis:

hereby :: thesis:

let b be Real; :: thesis:
assume A3: a <= b ; :: thesis:
A4: for c being Real st b <= c holds
( f is_integrable_on ['b,c'] & f | ['b,c'] is bounded )

proof

let c be Real; :: thesis:
assume A5: b <= c ; :: thesis:
then a <= c by A3, XXREAL_0:2;
then A6: ( f is_integrable_on ['a,c'] & f | ['a,c'] is bounded ) by A2, INTEGR10:def 5;
['a,c'] = [.a,c.] by A5, A3, XXREAL_0:2, INTEGRA5:def 3;
then ['a,c'] c= [.a,+infty.[ by XXREAL_1:251;
then ['a,c'] c= dom f by A1;
hence ( f is_integrable_on ['b,c'] & f | ['b,c'] is bounded ) by A3, A5, A6, INTEGRA6:18; :: thesis:

end;

consider I being PartFunc of REAL,REAL such that
A7: dom I = right_closed_halfline a and
A8: for x being Real st x in dom I holds
I . x = integral (f,a,x) and
A9: I is convergent_in+infty by A2, INTEGR10:def 5;
b < +infty by XREAL_0:def 1, XXREAL_0:9;
then reconsider B = [.b,+infty.[ as non empty Subset of REAL by XXREAL_1:3;
deffunc H₁( Element of B) -> Element of REAL = In ((integral (f,b,$1)),REAL);
consider Intf being Function of B,REAL such that
A10: for x being Element of B holds Intf . x = H₁(x) from FUNCT_2:sch 4();
A11: dom Intf = B by FUNCT_2:def 1;
then reconsider Intf = Intf as PartFunc of REAL,REAL by RELSET_1:5;
A12: dom Intf = right_closed_halfline b by FUNCT_2:def 1;
A13: for x being Real st x in dom Intf holds
Intf . x = integral (f,b,x)

proof

let x be Real; :: thesis:
assume x in dom Intf ; :: thesis:
then Intf . x = In ((integral (f,b,x)),REAL) by A10, A11;
hence Intf . x = integral (f,b,x) ; :: thesis:

end;

A14: for r being Real ex g being Real st
( r < g & g in dom Intf )

proof

let r be Real; :: thesis:
consider g being Real such that
A15: max (b,r) < g by XREAL_1:1;
A16: g < +infty by XXREAL_0:9, XREAL_0:def 1;
( r <= max (b,r) & b <= max (b,r) ) by XXREAL_0:25;
then A17: ( r < g & b < g ) by A15, XXREAL_0:2;
then g in [.b,+infty.[ by A16, XXREAL_1:3;
hence ex g being Real st
( r < g & g in dom Intf ) by A11, A17; :: thesis:

end;

consider G being Real such that
A18: for g1 being Real st 0 < g1 holds
ex r being Real st
for r1 being Real st r < r1 & r1 in dom I holds
|.((I . r1) - G).| < g1 by A9, LIMFUNC1:44;
set G1 = G - (integral (f,a,b));
for g1 being Real st 0 < g1 holds
ex r being Real st
for r1 being Real st r < r1 & r1 in dom Intf holds
|.((Intf . r1) - (G - (integral (f,a,b)))).| < g1

proof

let g1 be Real; :: thesis:
assume 0 < g1 ; :: thesis:
then consider R being Real such that
A19: for r1 being Real st R < r1 & r1 in dom I holds
|.((I . r1) - G).| < g1 by A18;
take R ; :: thesis:
thus for r1 being Real st R < r1 & r1 in dom Intf holds
|.((Intf . r1) - (G - (integral (f,a,b)))).| < g1 :: thesis:

proof

let r1 be Real; :: thesis:
assume that
A20: R < r1 and
A21: r1 in dom Intf ; :: thesis:
A22: [.b,+infty.[ c= [.a,+infty.[ by A3, XXREAL_1:38;
A23: b <= r1 by A21, A11, XXREAL_1:3;
then A24: a <= r1 by A3, XXREAL_0:2;
then A25: ( f is_integrable_on ['a,r1'] & f | ['a,r1'] is bounded ) by A2, INTEGR10:def 5;
A26: ['a,r1'] = [.a,r1.] by A23, A3, XXREAL_0:2, INTEGRA5:def 3;
then ['a,r1'] c= [.a,+infty.[ by XXREAL_1:251;
then A27: ['a,r1'] c= dom f by A1;
A28: b in ['a,r1'] by A3, A23, A26, XXREAL_1:1;
A29: (integral (f,a,b)) + (integral (f,b,r1)) = integral (f,a,r1) by A24, A25, A27, A28, INTEGRA6:17;
(Intf . r1) - (G - (integral (f,a,b))) = (integral (f,b,r1)) - (G - (integral (f,a,b))) by A13, A21;
then (Intf . r1) - (G - (integral (f,a,b))) = (integral (f,a,r1)) - G by A29;
then (Intf . r1) - (G - (integral (f,a,b))) = (I . r1) - G by A22, A21, A11, A7, A8;
hence |.((Intf . r1) - (G - (integral (f,a,b)))).| < g1 by A19, A20, A22, A21, A11, A7; :: thesis:

end;

end;

hence f is_+infty_ext_Riemann_integrable_on b by A4, A12, A13, A14, LIMFUNC1:44, INTEGR10:def 5; :: thesis:

end;