let f be PartFunc of REAL,REAL; :: thesis: for a, b, c being Real st a < b & b <= c & ].a,c.] c= dom f & f | ['b,c'] is bounded & f is_integrable_on ['b,c'] & f is_left_ext_Riemann_integrable_on a,b holds
( f is_left_ext_Riemann_integrable_on a,c & ext_left_integral (f,a,c) = (ext_left_integral (f,a,b)) + (integral (f,b,c)) )
let a, b, c be Real; :: thesis: ( a < b & b <= c & ].a,c.] c= dom f & f | ['b,c'] is bounded & f is_integrable_on ['b,c'] & f is_left_ext_Riemann_integrable_on a,b implies ( f is_left_ext_Riemann_integrable_on a,c & ext_left_integral (f,a,c) = (ext_left_integral (f,a,b)) + (integral (f,b,c)) ) )
assume that
A1: ( a < b & b <= c ) and
A2: ].a,c.] c= dom f and
A3: f | ['b,c'] is bounded and
A4: f is_integrable_on ['b,c'] and
A5: f is_left_ext_Riemann_integrable_on a,b ; :: thesis: ( f is_left_ext_Riemann_integrable_on a,c & ext_left_integral (f,a,c) = (ext_left_integral (f,a,b)) + (integral (f,b,c)) )
A6: a < c by A1, XXREAL_0:2;
A7: ( ['a,b'] = [.a,b.] & ['b,c'] = [.b,c.] & ['a,c'] = [.a,c.] ) by A1, XXREAL_0:2, INTEGRA5:def 3;
then ( ['a,b'] c= ['a,c'] & ['b,c'] c= ].a,c.] ) by A1, XXREAL_1:34, XXREAL_1:39;
then A8: ['b,c'] c= dom f by A2;
A9: for e being Real st a < e & e <= c holds
( f is_integrable_on ['e,c'] & f | ['e,c'] is bounded )

proof

let e be Real; :: thesis: ( a < e & e <= c implies ( f is_integrable_on ['e,c'] & f | ['e,c'] is bounded ) )
assume A10: ( a < e & e <= c ) ; :: thesis: ( f is_integrable_on ['e,c'] & f | ['e,c'] is bounded )

per cases ( b <= e or e < b ) ;

suppose A11: b <= e ; :: thesis: ( f is_integrable_on ['e,c'] & f | ['e,c'] is bounded )

then e in ['b,c'] by A7, A10, XXREAL_1:1;
hence f is_integrable_on ['e,c'] by A8, A1, A3, A4, INTEGRA6:17; :: thesis: f | ['e,c'] is bounded
['e,c'] = [.e,c.] by A10, INTEGRA5:def 3;
hence f | ['e,c'] is bounded by A3, A7, A11, XXREAL_1:34, RFUNCT_1:74; :: thesis: verum

end;

suppose A12: e < b ; :: thesis: ( f is_integrable_on ['e,c'] & f | ['e,c'] is bounded )

then A13: ( f is_integrable_on ['e,b'] & f | ['e,b'] is bounded ) by A5, A10, INTEGR10:def 2;
A14: ['e,c'] = [.e,c.] by A1, A12, XXREAL_0:2, INTEGRA5:def 3;
then ['e,c'] c= ].a,c.] by A10, XXREAL_1:39;
then ['e,c'] c= dom f by A2;
hence f is_integrable_on ['e,c'] by A1, A3, A4, A12, A13, Th1; :: thesis: f | ['e,c'] is bounded
['e,b'] = [.e,b.] by A12, INTEGRA5:def 3;
then ['e,c'] = ['e,b'] \/ ['b,c'] by A1, A7, A12, A14, XXREAL_1:165;
hence f | ['e,c'] is bounded by A3, A13, RFUNCT_1:87; :: thesis: verum

end;

end;

end;

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

proof

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

end;

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

proof

let r be Real; :: thesis: ( a < r implies ex g being Real st
( g < r & a < g & g in dom Intf ) )
assume a < r ; :: thesis: ex g being Real st
( g < r & a < g & g in dom Intf )
then consider g being Real such that
A22: ( a < g & g < min (r,c) ) by A6, XXREAL_0:21, XREAL_1:5;
take g ; :: thesis: ( g < r & a < g & g in dom Intf )
A23: ( r >= min (r,c) & c >= min (r,c) ) by XXREAL_0:17;
hence ( g < r & a < g ) by A22, XXREAL_0:2; :: thesis: g in dom Intf
( a < g & g < c ) by A22, A23, XXREAL_0:2;
hence g in dom Intf by A19, XXREAL_1:2; :: thesis: verum

end;

consider G being Real such that
A24: for g1 being Real st 0 < g1 holds
ex r being Real st
( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom I holds
|.((I . r1) - G).| < g1 ) ) by A17, LIMFUNC2:10;
set G1 = G + (integral (f,b,c));
A25: for g1 being Real st 0 < g1 holds
ex r being Real st
( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
|.((Intf . r1) - (G + (integral (f,b,c)))).| < g1 ) )

proof

let g1 be Real; :: thesis: ( 0 < g1 implies ex r being Real st
( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
|.((Intf . r1) - (G + (integral (f,b,c)))).| < g1 ) ) )
assume 0 < g1 ; :: thesis: ex r being Real st
( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
|.((Intf . r1) - (G + (integral (f,b,c)))).| < g1 ) )
then consider R being Real such that
A26: a < R and
A27: for r1 being Real st r1 < R & a < r1 & r1 in dom I holds
|.((I . r1) - G).| < g1 by A24;
set R1 = min (R,b);
take min (R,b) ; :: thesis: ( a < min (R,b) & ( for r1 being Real st r1 < min (R,b) & a < r1 & r1 in dom Intf holds
|.((Intf . r1) - (G + (integral (f,b,c)))).| < g1 ) )
thus a < min (R,b) by A26, A1, XXREAL_0:21; :: thesis: for r1 being Real st r1 < min (R,b) & a < r1 & r1 in dom Intf holds
|.((Intf . r1) - (G + (integral (f,b,c)))).| < g1
thus for r1 being Real st r1 < min (R,b) & a < r1 & r1 in dom Intf holds
|.((Intf . r1) - (G + (integral (f,b,c)))).| < g1 :: thesis: verum

proof

let r1 be Real; :: thesis: ( r1 < min (R,b) & a < r1 & r1 in dom Intf implies |.((Intf . r1) - (G + (integral (f,b,c)))).| < g1 )
assume that
A28: ( r1 < min (R,b) & a < r1 ) and
A29: r1 in dom Intf ; :: thesis: |.((Intf . r1) - (G + (integral (f,b,c)))).| < g1
min (R,b) <= R by XXREAL_0:17;
then A30: r1 < R by A28, XXREAL_0:2;
r1 <= c by A19, A29, XXREAL_1:2;
then ['r1,c'] = [.r1,c.] by INTEGRA5:def 3;
then ['r1,c'] c= ].a,c.] by A28, XXREAL_1:39;
then A31: ['r1,c'] c= dom f by A2;
min (R,b) <= b by XXREAL_0:17;
then A32: r1 <= b by A28, XXREAL_0:2;
then A33: r1 in dom I by A15, A28, XXREAL_1:2;
A34: ( f is_integrable_on ['r1,b'] & f | ['r1,b'] is bounded ) by A5, A28, A32, INTEGR10:def 2;
Intf . r1 = integral (f,r1,c) by A20, A29;
then (Intf . r1) - (G + (integral (f,b,c))) = ((integral (f,r1,c)) - (integral (f,b,c))) - G ;
then (Intf . r1) - (G + (integral (f,b,c))) = (((integral (f,r1,b)) + (integral (f,b,c))) - (integral (f,b,c))) - G by A31, A1, A3, A4, A32, A34, Th1;
then (Intf . r1) - (G + (integral (f,b,c))) = (I . r1) - G by A16, A28, A32, A15, XXREAL_1:2;
hence |.((Intf . r1) - (G + (integral (f,b,c)))).| < g1 by A30, A27, A28, A33; :: thesis: verum

end;

end;

hence A35: f is_left_ext_Riemann_integrable_on a,c by A9, A19, A20, A21, LIMFUNC2:10, INTEGR10:def 2; :: thesis: ext_left_integral (f,a,c) = (ext_left_integral (f,a,b)) + (integral (f,b,c))
A36: Intf is_right_convergent_in a by A21, A25, LIMFUNC2:10;
then A37: ext_left_integral (f,a,c) = lim_right (Intf,a) by A19, A20, A35, INTEGR10:def 4;
A38: ext_left_integral (f,a,b) = lim_right (I,a) by A5, A15, A16, A17, INTEGR10:def 4;
for g1 being Real st 0 < g1 holds
ex r being Real st
( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
|.((Intf . r1) - ((ext_left_integral (f,a,b)) + (integral (f,b,c)))).| < g1 ) )

proof

let g1 be Real; :: thesis: ( 0 < g1 implies ex r being Real st
( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
|.((Intf . r1) - ((ext_left_integral (f,a,b)) + (integral (f,b,c)))).| < g1 ) ) )
assume A39: 0 < g1 ; :: thesis: ex r being Real st
( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
|.((Intf . r1) - ((ext_left_integral (f,a,b)) + (integral (f,b,c)))).| < g1 ) )
consider r being Real such that
A40: ( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom I holds
|.((I . r1) - (ext_left_integral (f,a,b))).| < g1 ) ) by A39, A38, A17, LIMFUNC2:42;
set R = min (b,r);
for r1 being Real st r1 < min (b,r) & a < r1 & r1 in dom Intf holds
|.((Intf . r1) - ((ext_left_integral (f,a,b)) + (integral (f,b,c)))).| < g1

proof

let r1 be Real; :: thesis: ( r1 < min (b,r) & a < r1 & r1 in dom Intf implies |.((Intf . r1) - ((ext_left_integral (f,a,b)) + (integral (f,b,c)))).| < g1 )
assume A41: ( r1 < min (b,r) & a < r1 & r1 in dom Intf ) ; :: thesis: |.((Intf . r1) - ((ext_left_integral (f,a,b)) + (integral (f,b,c)))).| < g1
then ( r1 <= c & a < c ) by A1, A19, XXREAL_0:2, XXREAL_1:2;
then A42: ( [.r1,c.] = ['r1,c'] & [.a,c.] = ['a,c'] ) by INTEGRA5:def 3;
[.r1,c.] c= ].a,c.] by A41, XXREAL_1:39;
then A43: ['r1,c'] c= dom f by A42, A2;
( min (b,r) <= b & min (b,r) <= r ) by XXREAL_0:17;
then A44: ( r1 < b & r1 < r ) by A41, XXREAL_0:2;
then A45: r1 in dom I by A41, A15, XXREAL_1:2;
( f is_integrable_on ['r1,b'] & f | ['r1,b'] is bounded ) by A41, A44, A5, INTEGR10:def 2;
then integral (f,r1,c) = (integral (f,r1,b)) + (integral (f,b,c)) by A1, A43, A3, A4, A44, Th1;
then Intf . r1 = (integral (f,b,c)) + (integral (f,r1,b)) by A41, A20;
then (Intf . r1) - ((integral (f,b,c)) + (ext_left_integral (f,a,b))) = (integral (f,r1,b)) - (ext_left_integral (f,a,b))
.= (I . r1) - (ext_left_integral (f,a,b)) by A44, A16, A41, A15, XXREAL_1:2 ;
hence |.((Intf . r1) - ((ext_left_integral (f,a,b)) + (integral (f,b,c)))).| < g1 by A40, A41, A45, A44; :: thesis: verum

end;

hence ex r being Real st
( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
|.((Intf . r1) - ((ext_left_integral (f,a,b)) + (integral (f,b,c)))).| < g1 ) ) by A1, A40, XXREAL_0:21; :: thesis: verum

end;

hence ext_left_integral (f,a,c) = (ext_left_integral (f,a,b)) + (integral (f,b,c)) by A36, A37, LIMFUNC2:42; :: thesis: verum