let f be PartFunc of REAL,REAL; :: thesis: for a, b being Real st ].a,b.] c= dom f & f is_left_ext_Riemann_integrable_on a,b holds
for d being Real st a < d & d <= b holds
( f is_left_ext_Riemann_integrable_on a,d & ext_left_integral (f,a,b) = (ext_left_integral (f,a,d)) + (integral (f,d,b)) )
let a, b be Real; :: thesis: ( ].a,b.] c= dom f & f is_left_ext_Riemann_integrable_on a,b implies for d being Real st a < d & d <= b holds
( f is_left_ext_Riemann_integrable_on a,d & ext_left_integral (f,a,b) = (ext_left_integral (f,a,d)) + (integral (f,d,b)) ) )
assume that
A1: ].a,b.] c= dom f and
A2: f is_left_ext_Riemann_integrable_on a,b ; :: thesis: for d being Real st a < d & d <= b holds
( f is_left_ext_Riemann_integrable_on a,d & ext_left_integral (f,a,b) = (ext_left_integral (f,a,d)) + (integral (f,d,b)) )

hereby :: thesis: verum

let d be Real; :: thesis: ( a < d & d <= b implies ( f is_left_ext_Riemann_integrable_on a,d & ext_left_integral (f,a,b) = (ext_left_integral (f,a,d)) + (integral (f,d,b)) ) )
assume that
A3: a < d and
A4: d <= b ; :: thesis: ( f is_left_ext_Riemann_integrable_on a,d & ext_left_integral (f,a,b) = (ext_left_integral (f,a,d)) + (integral (f,d,b)) )
A5: for c being Real st a < c & c <= d holds
( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded )

proof

let c be Real; :: thesis: ( a < c & c <= d implies ( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded ) )
assume A6: ( a < c & c <= d ) ; :: thesis: ( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded )
then ( a < c & c <= b ) by A4, XXREAL_0:2;
then A7: ( f is_integrable_on ['c,b'] & f | ['c,b'] is bounded ) by A2, INTEGR10:def 2;
A8: ( ['c,d'] = [.c,d.] & ['c,b'] = [.c,b.] ) by A6, A4, XXREAL_0:2, INTEGRA5:def 3;
then ['c,b'] c= ].a,b.] by A6, XXREAL_1:39;
then ['c,b'] c= dom f by A1;
hence f is_integrable_on ['c,d'] by A4, A6, A7, INTEGRA6:18; :: thesis: f | ['c,d'] is bounded
thus f | ['c,d'] is bounded by A7, A8, A4, XXREAL_1:34, RFUNCT_1:74; :: thesis: verum

end;

consider I being PartFunc of REAL,REAL such that
A9: dom I = ].a,b.] and
A10: for x being Real st x in dom I holds
I . x = integral (f,x,b) and
A11: I is_right_convergent_in a by A2, INTEGR10:def 2;
reconsider AB = ].a,d.] as non empty Subset of REAL by A3, XXREAL_1:2;
deffunc H₁( Element of AB) -> Element of REAL = In ((integral (f,$1,d)),REAL);
consider Intf being Function of AB,REAL such that
A12: for x being Element of AB holds Intf . x = H₁(x) from FUNCT_2:sch 4();
A13: dom Intf = AB by FUNCT_2:def 1;
then reconsider Intf = Intf as PartFunc of REAL,REAL by RELSET_1:5;
A14: for x being Real st x in dom Intf holds
Intf . x = integral (f,x,d)

proof

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

end;

A15: 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
A16: ( a < g & g < min (r,d) ) by A3, XXREAL_0:21, XREAL_1:5;
take g ; :: thesis: ( g < r & a < g & g in dom Intf )
A17: ( min (r,d) <= r & min (r,d) <= d ) by XXREAL_0:17;
hence ( g < r & a < g ) by A16, XXREAL_0:2; :: thesis: g in dom Intf
( a < g & g < d ) by A16, A17, XXREAL_0:2;
hence g in dom Intf by A13, XXREAL_1:2; :: thesis: verum

end;

consider G being Real such that
A18: 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 A11, LIMFUNC2:10;
set G1 = G - (integral (f,d,b));
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,d,b)))).| < 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,d,b)))).| < 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,d,b)))).| < g1 ) )
then consider R being Real such that
A19: a < R and
A20: for r1 being Real st r1 < R & a < r1 & r1 in dom I holds
|.((I . r1) - G).| < g1 by A18;
take R ; :: thesis: ( a < R & ( for r1 being Real st r1 < R & a < r1 & r1 in dom Intf holds
|.((Intf . r1) - (G - (integral (f,d,b)))).| < g1 ) )
thus a < R by A19; :: thesis: for r1 being Real st r1 < R & a < r1 & r1 in dom Intf holds
|.((Intf . r1) - (G - (integral (f,d,b)))).| < g1
thus for r1 being Real st r1 < R & a < r1 & r1 in dom Intf holds
|.((Intf . r1) - (G - (integral (f,d,b)))).| < g1 :: thesis: verum

proof

let r1 be Real; :: thesis: ( r1 < R & a < r1 & r1 in dom Intf implies |.((Intf . r1) - (G - (integral (f,d,b)))).| < g1 )
assume that
A21: ( r1 < R & a < r1 ) and
A22: r1 in dom Intf ; :: thesis: |.((Intf . r1) - (G - (integral (f,d,b)))).| < g1
A23: r1 <= d by A13, A22, XXREAL_1:2;
then A24: r1 <= b by A4, XXREAL_0:2;
then A25: r1 in dom I by A9, A21, XXREAL_1:2;
A26: f is_integrable_on ['r1,b'] by A21, A24, A2, INTEGR10:def 2;
A27: f | ['r1,b'] is bounded by A21, A24, A2, INTEGR10:def 2;
A28: ['r1,b'] = [.r1,b.] by A23, A4, XXREAL_0:2, INTEGRA5:def 3;
then ['r1,b'] c= ].a,b.] by A21, XXREAL_1:39;
then A29: ['r1,b'] c= dom f by A1;
A30: d in ['r1,b'] by A4, A28, A23, XXREAL_1:1;
A31: b in ['r1,b'] by A24, A28, XXREAL_1:1;
Intf . r1 = integral (f,r1,d) by A14, A22;
then (Intf . r1) - (G - (integral (f,d,b))) = ((integral (f,r1,d)) + (integral (f,d,b))) - G ;
then (Intf . r1) - (G - (integral (f,d,b))) = (integral (f,r1,b)) - G by A26, A27, A29, A30, A31, A23, A4, XXREAL_0:2, INTEGRA6:20;
then (Intf . r1) - (G - (integral (f,d,b))) = (I . r1) - G by A21, A10, A24, A9, XXREAL_1:2;
hence |.((Intf . r1) - (G - (integral (f,d,b)))).| < g1 by A20, A21, A25; :: thesis: verum

end;

end;

hence A32: f is_left_ext_Riemann_integrable_on a,d by A5, A13, A14, A15, LIMFUNC2:10, INTEGR10:def 2; :: thesis: ext_left_integral (f,a,b) = (ext_left_integral (f,a,d)) + (integral (f,d,b))
( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded ) by A3, A4, A2, INTEGR10:def 2;
hence ext_left_integral (f,a,b) = (ext_left_integral (f,a,d)) + (integral (f,d,b)) by A3, A4, A1, A32, Th20; :: thesis: verum

end;