let f be PartFunc of REAL,REAL; :: thesis:
let a, b be Real; :: thesis:
assume that
A1: a <= b and
A2: left_closed_halfline b 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 a ; :: thesis:
A6: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
A7: for c being Real st c <= b holds
( f is_integrable_on ['c,b'] & f | ['c,b'] is bounded )

proof

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

per cases ;

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

['a,b'] c= ].-infty,b.] by A6, XXREAL_1:265;
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 ['c,b'] by A1, A3, A4, A11, INTEGRA6:17; :: thesis:
thus f | ['c,b'] is bounded by A4, A6, A9, A10, XXREAL_1:34, RFUNCT_1:74; :: thesis:

end;

suppose A12: c < a ; :: thesis:

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

end;

end;

end;

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

proof

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

end;

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

proof

let r be Real; :: thesis:
consider g being Real such that
A22: g < min (b,r) by XREAL_1:2;
A23: -infty < g by XREAL_0:def 1, XXREAL_0:12;
( min (b,r) <= r & min (b,r) <= b ) by XXREAL_0:17;
then A24: ( g < r & g < b ) by A22, XXREAL_0:2;
then g in ].-infty,b.] by A23, XXREAL_1:2;
hence ex g being Real st
( g < r & 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 r1 < r & r1 in dom I holds
|.((I . r1) - G).| < g1 by A16, LIMFUNC1:45;
G = lim_in-infty I by A25, A16, LIMFUNC1:78;
then A26: G = infty_ext_left_integral (f,a) by A5, A14, A15, A16, INTEGR10:def 8;
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 r1 < r & 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 r1 < R & r1 in dom I holds
|.((I . r1) - G).| < g1 by A25;
set R1 = min (R,a);
take min (R,a) ; :: thesis:
thus for r1 being Real st r1 < min (R,a) & r1 in dom Intf holds
|.((Intf . r1) - (G + (integral (f,a,b)))).| < g1 :: thesis:

proof

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

end;

end;

hence A39: f is_-infty_ext_Riemann_integrable_on b by A7, A19, A20, A21, LIMFUNC1:45, INTEGR10:def 6; :: thesis:
A40: Intf is convergent_in-infty by A21, A27, LIMFUNC1:45;
then infty_ext_left_integral (f,b) = lim_in-infty Intf by A19, A20, A39, INTEGR10:def 8;
hence infty_ext_left_integral (f,b) = (infty_ext_left_integral (f,a)) + (integral (f,a,b)) by A40, A26, A27, LIMFUNC1:78; :: thesis: