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 | ['a,b'] is bounded & f is_integrable_on ['a,b'] & f is_right_ext_Riemann_integrable_on b,c holds
( f is_right_ext_Riemann_integrable_on a,c & ext_right_integral (f,a,c) = (integral (f,a,b)) + (ext_right_integral (f,b,c)) )
let a, b, c be Real; :: thesis: ( a <= b & b < c & [.a,c.[ c= dom f & f | ['a,b'] is bounded & f is_integrable_on ['a,b'] & f is_right_ext_Riemann_integrable_on b,c implies ( f is_right_ext_Riemann_integrable_on a,c & ext_right_integral (f,a,c) = (integral (f,a,b)) + (ext_right_integral (f,b,c)) ) )
assume that
A1: ( a <= b & b < c ) and
A2: [.a,c.[ c= dom f and
A3: f | ['a,b'] is bounded and
A4: f is_integrable_on ['a,b'] and
A5: f is_right_ext_Riemann_integrable_on b,c ; :: thesis: ( f is_right_ext_Riemann_integrable_on a,c & ext_right_integral (f,a,c) = (integral (f,a,b)) + (ext_right_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:43;
then A8: ['a,b'] c= dom f by A2;
A9: for e being Real st a <= e & e < c holds
( f is_integrable_on ['a,e'] & f | ['a,e'] is bounded )

proof

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

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

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

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

end;

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

then A13: ( f is_integrable_on ['b,e'] & f | ['b,e'] is bounded ) by A5, A10, INTEGR10:def 1;
A14: ['a,e'] = [.a,e.] by A1, A12, XXREAL_0:2, INTEGRA5:def 3;
then ['a,e'] c= [.a,c.[ by A10, XXREAL_1:43;
then ['a,e'] c= dom f by A2;
hence f is_integrable_on ['a,e'] by A1, A3, A4, A12, A13, Th1; :: thesis: f | ['a,e'] is bounded
['b,e'] = [.b,e.] by A12, INTEGRA5:def 3;
then ['a,e'] = ['a,b'] \/ ['b,e'] by A1, A7, A12, A14, XXREAL_1:165;
hence f | ['a,e'] 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 = [.b,c.[ and
A16: for x being Real st x in dom I holds
I . x = integral (f,b,x) and
A17: I is_left_convergent_in c by A5, INTEGR10:def 1;
reconsider AC = [.a,c.[ as non empty Subset of REAL by A1, XXREAL_1:3;
deffunc H₁( Element of AC) -> Element of REAL = In ((integral (f,a,$1)),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,a,x)

proof

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

end;

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

proof

let r be Real; :: thesis: ( r < c implies ex g being Real st
( r < g & g < c & g in dom Intf ) )
assume r < c ; :: thesis: ex g being Real st
( r < g & g < c & g in dom Intf )
then consider g being Real such that
A22: ( max (r,a) < g & g < c ) by A6, XXREAL_0:29, XREAL_1:5;
take g ; :: thesis: ( r < g & g < c & g in dom Intf )
A23: ( r <= max (r,a) & a <= max (r,a) ) by XXREAL_0:25;
hence ( r < g & g < c ) 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:3; :: thesis: verum

end;

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

proof

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

proof

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

end;

end;

hence A34: f is_right_ext_Riemann_integrable_on a,c by A9, A19, A20, A21, LIMFUNC2:7, INTEGR10:def 1; :: thesis: ext_right_integral (f,a,c) = (integral (f,a,b)) + (ext_right_integral (f,b,c))
A35: Intf is_left_convergent_in c by A25, A21, LIMFUNC2:7;
then A36: ext_right_integral (f,a,c) = lim_left (Intf,c) by A19, A20, A34, INTEGR10:def 3;
A37: ext_right_integral (f,b,c) = lim_left (I,c) by A5, A15, A16, A17, INTEGR10:def 3;
for g1 being Real st 0 < g1 holds
ex r being Real st
( r < c & ( for r1 being Real st r < r1 & r1 < c & r1 in dom Intf holds
|.((Intf . r1) - ((integral (f,a,b)) + (ext_right_integral (f,b,c)))).| < g1 ) )

proof

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

proof

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

end;

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

end;

hence ext_right_integral (f,a,c) = (integral (f,a,b)) + (ext_right_integral (f,b,c)) by A35, A36, LIMFUNC2:41; :: thesis: verum