let f be PartFunc of REAL,REAL; :: thesis:
let a, b be Real; :: thesis:
assume that
A1: [.a,b.[ c= dom f and
A2: f is_right_ext_Riemann_integrable_on a,b ; :: thesis:

hereby :: thesis:

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

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

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,a,x) and
A11: I is_left_convergent_in b by A2, INTEGR10:def 1;
reconsider AB = [.c,b.[ as non empty Subset of REAL by A4, XXREAL_1:3;
deffunc H₁( Element of AB) -> Element of REAL = In ((integral (f,c,$1)),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,c,x)

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

end;

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

let r be Real; :: thesis:
assume r < b ; :: thesis:
then consider g being Real such that
A16: ( max (r,c) < g & g < b ) by A4, XXREAL_0:29, XREAL_1:5;
take g ; :: thesis:
A17: ( r <= max (r,c) & c <= max (r,c) ) by XXREAL_0:25;
hence ( r < g & g < b ) by A16, XXREAL_0:2; :: thesis:
( c < g & g < b ) by A16, A17, XXREAL_0:2;
hence g in dom Intf by A13, XXREAL_1:3; :: thesis:

end;

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

let g1 be Real; :: thesis:
assume 0 < g1 ; :: thesis:
then consider R being Real such that
A19: R < b and
A20: for r1 being Real st R < r1 & r1 < b & r1 in dom I holds
|.((I . r1) - G).| < g1 by A18;
take R ; :: thesis:
thus R < b by A19; :: thesis:
thus for r1 being Real st R < r1 & r1 < b & r1 in dom Intf holds
|.((Intf . r1) - (G - (integral (f,a,c)))).| < g1 :: thesis:

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

end;

end;

hence A31: f is_right_ext_Riemann_integrable_on c,b by A5, A13, A14, A15, LIMFUNC2:7, INTEGR10:def 1; :: thesis:
( f is_integrable_on ['a,c'] & f | ['a,c'] is bounded ) by A2, A3, A4, INTEGR10:def 1;
hence ext_right_integral (f,a,b) = (integral (f,a,c)) + (ext_right_integral (f,c,b)) by A3, A4, A1, A31, Th21; :: thesis:

end;