let f be PartFunc of REAL,REAL; :: thesis:
let a, b be Real; :: thesis:
assume that
A1: a <= b and
A2: right_closed_halfline a c= dom f and
A3: f is_integrable_on ['a,b'] and
A4: f | ['a,b'] is bounded and
A5: f is_+infty_ext_Riemann_integrable_on b ; :: thesis:
A6: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
A7: for c being Real st a <= c holds
( f is_integrable_on ['a,c'] & f | ['a,c'] is bounded )

proof

let c be Real; :: thesis:
assume A8: a <= c ; :: thesis:
then A9: ['a,c'] = [.a,c.] by INTEGRA5:def 3;

per cases ;

suppose A10: c <= b ; :: thesis:

['a,b'] c= [.a,+infty.[ by A6, XXREAL_1:251;
then A11: ['a,b'] c= dom f by A2;
c in ['a,b'] by A8, A10, A6, XXREAL_1:1;
hence f is_integrable_on ['a,c'] by A1, A3, A4, A11, INTEGRA6:17; :: thesis:
thus f | ['a,c'] is bounded by A4, A6, A9, A10, XXREAL_1:34, RFUNCT_1:74; :: thesis:

end;

suppose A12: b < c ; :: thesis:

then A13: ( f is_integrable_on ['b,c'] & f | ['b,c'] is bounded ) by A5, INTEGR10:def 5;
['a,c'] c= [.a,+infty.[ by A9, XXREAL_1:251;
then ['a,c'] c= dom f by A2;
hence f is_integrable_on ['a,c'] by A1, A12, A4, A13, A3, INTEGR24:1; :: thesis:
['b,c'] = [.b,c.] by A12, INTEGRA5:def 3;
then ['a,c'] = ['a,b'] \/ ['b,c'] by A1, A6, A9, A12, XXREAL_1:165;
hence f | ['a,c'] is bounded by A4, A13, RFUNCT_1:87; :: thesis:

end;

end;

end;

consider I being PartFunc of REAL,REAL such that
A14: dom I = right_closed_halfline b and
A15: for x being Real st x in dom I holds
I . x = integral (f,b,x) and
A16: I is convergent_in+infty by A5, INTEGR10:def 5;
a < +infty by XREAL_0:def 1, XXREAL_0:9;
then reconsider A = [.a,+infty.[ as non empty Subset of REAL by XXREAL_1:3;
deffunc H₁( Element of A) -> Element of REAL = In ((integral (f,a,$1)),REAL);
consider Intf being Function of A,REAL such that
A17: for x being Element of A holds Intf . x = H₁(x) from FUNCT_2:sch 4();
A18: dom Intf = A by FUNCT_2:def 1;
then reconsider Intf = Intf as PartFunc of REAL,REAL by RELSET_1:5;
A19: dom Intf = right_closed_halfline a by FUNCT_2:def 1;
A20: for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x)

proof

let x be Real; :: thesis:
assume x in dom Intf ; :: thesis:
then Intf . x = In ((integral (f,a,x)),REAL) by A17, A18;
hence Intf . x = integral (f,a,x) ; :: thesis:

end;

A21: 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
A22: max (a,r) < g by XREAL_1:1;
A23: g < +infty by XREAL_0:def 1, XXREAL_0:9;
( r <= max (a,r) & a <= max (a,r) ) by XXREAL_0:25;
then A24: ( r < g & a < g ) by A22, XXREAL_0:2;
then g in [.a,+infty.[ by A23, XXREAL_1:3;
hence ex g being Real st
( r < g & g in dom Intf ) by A18, A24; :: thesis:

end;

consider G being Real such that
A25: 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 A16, LIMFUNC1:44;
G = lim_in+infty I by A25, A16, LIMFUNC1:79;
then A26: G = infty_ext_right_integral (f,b) by A5, A14, A15, A16, INTEGR10:def 7;
set G1 = G + (integral (f,a,b));
A27: 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
A28: for r1 being Real st R < r1 & r1 in dom I holds
|.((I . r1) - G).| < g1 by A25;
set R1 = max (R,b);
take max (R,b) ; :: thesis:
thus for r1 being Real st max (R,b) < r1 & r1 in dom Intf holds
|.((Intf . r1) - (G + (integral (f,a,b)))).| < g1 :: thesis:

proof

let r1 be Real; :: thesis:
assume that
A29: max (R,b) < r1 and
A30: r1 in dom Intf ; :: thesis:
A31: ( b <= max (R,b) & R <= max (R,b) ) by XXREAL_0:25;
then A32: ( b < r1 & R < r1 ) by A29, XXREAL_0:2;
A33: r1 in dom I by A14, A31, A29, XXREAL_0:2, XXREAL_1:236;
A34: a <= r1 by A1, A32, XXREAL_0:2;
then A35: ( f is_integrable_on ['a,r1'] & f | ['a,r1'] is bounded ) by A7;
A36: ['a,r1'] = [.a,r1.] by A1, A32, XXREAL_0:2, INTEGRA5:def 3;
then ['a,r1'] c= [.a,+infty.[ by XXREAL_1:251;
then A37: ['a,r1'] c= dom f by A2;
A38: b in ['a,r1'] by A1, A32, A36, XXREAL_1:1;
A39: (integral (f,a,b)) + (integral (f,b,r1)) = integral (f,a,r1) by A34, A35, A37, A38, INTEGRA6:17;
(Intf . r1) - (G + (integral (f,a,b))) = (integral (f,a,r1)) - (G + (integral (f,a,b))) by A20, A30;
then (Intf . r1) - (G + (integral (f,a,b))) = (integral (f,b,r1)) - G by A39;
then (Intf . r1) - (G + (integral (f,a,b))) = (I . r1) - G by A32, A15, A14, XXREAL_1:236;
hence |.((Intf . r1) - (G + (integral (f,a,b)))).| < g1 by A28, A33, A32; :: thesis:

end;

end;

hence A40: f is_+infty_ext_Riemann_integrable_on a by A7, A19, A20, A21, LIMFUNC1:44, INTEGR10:def 5; :: thesis:
A41: Intf is convergent_in+infty by A21, A27, LIMFUNC1:44;
then infty_ext_right_integral (f,a) = lim_in+infty Intf by A19, A20, A40, INTEGR10:def 7;
hence infty_ext_right_integral (f,a) = (infty_ext_right_integral (f,b)) + (integral (f,a,b)) by A41, A26, A27, LIMFUNC1:79; :: thesis: