let f, g be PartFunc of REAL,REAL; :: thesis:
let a, b be Real; :: thesis:
assume that
A1: a < b and
A2: ( [.a,b.[ c= dom f & [.a,b.[ c= dom g ) and
A3: f is_right_ext_Riemann_integrable_on a,b and
A4: g is_right_ext_Riemann_integrable_on a,b ; :: thesis:
consider Intg being PartFunc of REAL,REAL such that
A5: dom Intg = [.a,b.[ and
A6: for x being Real st x in dom Intg holds
Intg . x = integral (g,a,x) and
A7: Intg is_left_convergent_in b and
A8: ext_right_integral (g,a,b) = lim_left (Intg,b) by A4, INTEGR10:def 3;
consider Intf being PartFunc of REAL,REAL such that
A9: dom Intf = [.a,b.[ and
A10: for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) and
A11: Intf is_left_convergent_in b and
A12: ext_right_integral (f,a,b) = lim_left (Intf,b) by A3, INTEGR10:def 3;
set Intfg = Intf + Intg;
A13: ( 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 A14: dom (Intf + Intg) = (dom Intf) /\ (dom Intg) by VALUED_1:def 1
.= [.a,b.[ by A9, A5 ; :: thesis:
let x be Real; :: thesis:
assume A15: x in dom (Intf + Intg) ; :: thesis:
then A16: x < b by A14, XXREAL_1:3;
then A17: [.a,x.] c= [.a,b.[ by XXREAL_1:43;
A18: a <= x by A14, A15, XXREAL_1:3;
then A19: ( f is_integrable_on ['a,x'] & f | ['a,x'] is bounded ) by A3, A16, INTEGR10:def 1;
['a,x'] = [.a,x.] by A18, INTEGRA5:def 3;
then A20: ( ['a,x'] c= dom f & ['a,x'] c= dom g ) by A2, A17;
A21: ( g is_integrable_on ['a,x'] & g | ['a,x'] is bounded ) by A4, A18, A16, INTEGR10:def 1;
thus (Intf + Intg) . x = (Intf . x) + (Intg . x) by A15, VALUED_1:def 1
.= (integral (f,a,x)) + (Intg . x) by A9, A10, A14, A15
.= (integral (f,a,x)) + (integral (g,a,x)) by A5, A6, A14, A15
.= integral ((f + g),a,x) by A18, A20, A19, A21, INTEGRA6:12 ; :: thesis:

end;

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

proof

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

per cases ;

suppose A24: r < a ; :: thesis:

take g = a; :: thesis:
thus ( r < g & g < b & g in dom (Intf + Intg) ) by A1, A13, A24, XXREAL_1:3; :: thesis:

end;

suppose not r < a ; :: thesis:

then A25: a - a <= r - a by XREAL_1:9;
take g = r + ((b - r) / 2); :: thesis:
A26: 0 < b - r by A23, XREAL_1:50;
then (b - r) / 2 < b - r by XREAL_1:216;
then A27: ((b - r) / 2) + r < (b - r) + r by XREAL_1:8;
r < g by A26, XREAL_1:29, XREAL_1:215;
then A28: r - (r - a) < g - 0 by A25, XREAL_1:14;
0 < (b - r) / 2 by A26, XREAL_1:215;
hence ( r < g & g < b & g in dom (Intf + Intg) ) by A13, A28, A27, XREAL_1:8, XXREAL_1:3; :: thesis:

end;

end;

end;

then A29: Intf + Intg is_left_convergent_in b by A11, A7, LIMFUNC2:45;
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 A30: ( a <= d & d < b ) ; :: thesis:
then ( ['a,d'] = [.a,d.] & [.a,d.] c= [.a,b.[ ) by INTEGRA5:def 3, XXREAL_1:43;
then A31: ( ['a,d'] c= dom f & ['a,d'] c= dom g ) by A2;
A32: ( f is_integrable_on ['a,d'] & g is_integrable_on ['a,d'] ) by A3, A4, A30, INTEGR10:def 1;
A33: ( f | ['a,d'] is bounded & g | ['a,d'] is bounded ) by A3, A4, A30, INTEGR10:def 1;
then (f + g) | (['a,d'] /\ ['a,d']) is bounded by RFUNCT_1:83;
hence ( f + g is_integrable_on ['a,d'] & (f + g) | ['a,d'] is bounded ) by A31, A32, A33, INTEGRA6:11; :: thesis:

end;

hence A34: f + g is_right_ext_Riemann_integrable_on a,b by A13, A22, A11, A7, LIMFUNC2:45, INTEGR10:def 1; :: thesis:
lim_left ((Intf + Intg),b) = (ext_right_integral (f,a,b)) + (ext_right_integral (g,a,b)) by A11, A12, A7, A8, A22, LIMFUNC2:45;
hence ext_right_integral ((f + g),a,b) = (ext_right_integral (f,a,b)) + (ext_right_integral (g,a,b)) by A13, A29, A34, INTEGR10:def 3; :: thesis: