let f, g be PartFunc of REAL ,REAL ; :: thesis:
let a, b be Real; :: thesis:
assume A1: ( a < b & ['a,b'] c= dom f & ['a,b'] c= dom g & f is_right_ext_Riemann_integrable_on a,b & g is_right_ext_Riemann_integrable_on a,b ) ; :: thesis:
consider Intf being PartFunc of REAL ,REAL such that
A2: ( dom Intf = [.a,b.[ & ( for x being Real st x in dom Intf holds
Intf . x = integral f,a,x ) & Intf is_left_convergent_in b & ext_right_integral f,a,b = lim_left Intf,b ) by Def3, A1;
consider Intg being PartFunc of REAL ,REAL such that
A3: ( dom Intg = [.a,b.[ & ( for x being Real st x in dom Intg holds
Intg . x = integral g,a,x ) & Intg is_left_convergent_in b & ext_right_integral g,a,b = lim_left Intg,b ) by Def3, A1;
set Intfg = Intf + Intg;
A4: for d being Real st a <= d & d < b holds
( f + g is_integrable_on ['a,d'] & (f + g) | ['a,d'] is bounded )

proof

let d be Real; :: thesis:
assume A5: ( a <= d & d < b ) ; :: thesis:
A6: ['a,d'] = [.a,d.] by INTEGRA5:def 4, A5;
A7: ['a,b'] = [.a,b.] by INTEGRA5:def 4, A1;
A8: [.a,d.] c= [.a,b.] by A5, XXREAL_1:34;
then A9: ['a,d'] c= dom f by A7, A6, A1, XBOOLE_1:1;
A10: ['a,d'] c= dom g by A7, A6, A8, A1, XBOOLE_1:1;
A11: ( f is_integrable_on ['a,d'] & f | ['a,d'] is bounded ) by A5, Def1, A1;
A12: ( g is_integrable_on ['a,d'] & g | ['a,d'] is bounded ) by A5, Def1, A1;
(f + g) | (['a,d'] /\ ['a,d']) is bounded by A11, A12, RFUNCT_1:100;
hence ( f + g is_integrable_on ['a,d'] & (f + g) | ['a,d'] is bounded ) by A11, A12, A9, A10, INTEGRA6:11; :: thesis:

end;

R2: ( dom (Intf + Intg) = [.a,b.[ & ( for x being Real st x in dom (Intf + Intg) holds
(Intf + Intg) . x = integral (f + g),a,x ) )

proof

thus A13: dom (Intf + Intg) = (dom Intf) /\ (dom Intg) by VALUED_1:def 1
.= [.a,b.[ by A2, A3 ; :: thesis:
let x be Real; :: thesis:
assume A14: x in dom (Intf + Intg) ; :: thesis:
then A15: ( a <= x & x < b ) by A13, XXREAL_1:3;
A16: ['a,x'] = [.a,x.] by INTEGRA5:def 4, A15;
A17: ['a,b'] = [.a,b.] by INTEGRA5:def 4, A1;
A18: [.a,x.] c= [.a,b.] by A15, XXREAL_1:34;
then A19: ['a,x'] c= dom f by A17, A16, A1, XBOOLE_1:1;
A20: ['a,x'] c= dom g by A17, A18, A1, XBOOLE_1:1, A16;
A21: ( f is_integrable_on ['a,x'] & f | ['a,x'] is bounded ) by A15, Def1, A1;
A22: ( g is_integrable_on ['a,x'] & g | ['a,x'] is bounded ) by A15, Def1, A1;
thus (Intf + Intg) . x = (Intf . x) + (Intg . x) by VALUED_1:def 1, A14
.= (integral f,a,x) + (Intg . x) by A2, A13, A14
.= (integral f,a,x) + (integral g,a,x) by A3, A13, A14
.= integral (f + g),a,x by A19, A20, A21, A22, INTEGRA6:12, A15 ; :: thesis:

end;

A23: ( Intf + Intg is_left_convergent_in b & lim_left (Intf + Intg),b = (ext_right_integral f,a,b) + (ext_right_integral g,a,b) )

proof

A24: for r being Element of REAL st r < b holds
ex g being Element of REAL st
( r < g & g < b & g in dom (Intf + Intg) )

proof

let r be Real; :: thesis:
assume A25: r < b ; :: thesis:

per cases ;

suppose A26: r < a ; :: thesis:

reconsider g = a as Real ;
take g ; :: thesis:
thus ( r < g & g < b & g in dom (Intf + Intg) ) by A26, A1, R2, XXREAL_1:3; :: thesis:

end;

suppose A27: not r < a ; :: thesis:

reconsider g = r + ((b - r) / 2) as Real ;
take g ; :: thesis:
0 < b - r by A25, XREAL_1:52;
then A28: ( 0 < (b - r) / 2 & (b - r) / 2 < b - r ) by XREAL_1:217, XREAL_1:218;
then A29: r < g by XREAL_1:31;
a - a <= r - a by A27, XREAL_1:11;
then A30: r - (r - a) < g - 0 by A29, XREAL_1:16;
((b - r) / 2) + r < (b - r) + r by A28, XREAL_1:10;
hence ( r < g & g < b & g in dom (Intf + Intg) ) by A28, R2, A30, XXREAL_1:3, XREAL_1:10; :: thesis:

end;

thus Intf + Intg is_left_convergent_in b by LIMFUNC2:53, A2, A3, A24; :: thesis:
thus lim_left (Intf + Intg),b = (ext_right_integral f,a,b) + (ext_right_integral g,a,b) by A3, A2, LIMFUNC2:53, A24; :: thesis:

end;

thus f + g is_right_ext_Riemann_integrable_on a,b by A4, R2, A23, Def1; :: thesis:
hence ext_right_integral (f + g),a,b = (ext_right_integral f,a,b) + (ext_right_integral g,a,b) by R2, A23, Def3; :: thesis: