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_left_ext_Riemann_integrable_on a,b and
A4: g is_left_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,x,b) and
A7: Intg is_right_convergent_in a and
A8: ext_left_integral (g,a,b) = lim_right (Intg,a) by A4, INTEGR10:def 4;
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,x,b) and
A11: Intf is_right_convergent_in a and
A12: ext_left_integral (f,a,b) = lim_right (Intf,a) by A3, INTEGR10:def 4;
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),x,b) ) )

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: a < x by A14, XXREAL_1:2;
then A17: [.x,b.] c= ].a,b.] by XXREAL_1:39;
A18: x <= b by A14, A15, XXREAL_1:2;
then A19: ( f is_integrable_on ['x,b'] & f | ['x,b'] is bounded ) by A3, A16, INTEGR10:def 2;
['x,b'] = [.x,b.] by A18, INTEGRA5:def 3;
then A20: ( ['x,b'] c= dom f & ['x,b'] c= dom g ) by A2, A17;
A21: ( g is_integrable_on ['x,b'] & g | ['x,b'] is bounded ) by A4, A16, A18, INTEGR10:def 2;
thus (Intf + Intg) . x = (Intf . x) + (Intg . x) by A15, VALUED_1:def 1
.= (integral (f,x,b)) + (Intg . x) by A9, A10, A14, A15
.= (integral (f,x,b)) + (integral (g,x,b)) by A5, A6, A14, A15
.= integral ((f + g),x,b) by A18, A20, A19, A21, INTEGRA6:12 ; :: thesis:

end;

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

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

suppose A24: b < r ; :: thesis:

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

end;

suppose A25: not b < r ; :: thesis:

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

end;

end;

end;

then A28: Intf + Intg is_right_convergent_in a by A11, A7, LIMFUNC2:54;
for d being Real st a < d & d <= b holds
( f + g is_integrable_on ['d,b'] & (f + g) | ['d,b'] is bounded )

let d be Real; :: thesis:
assume A29: ( a < d & d <= b ) ; :: thesis:
then ( ['d,b'] = [.d,b.] & [.d,b.] c= ].a,b.] ) by INTEGRA5:def 3, XXREAL_1:39;
then A30: ( ['d,b'] c= dom f & ['d,b'] c= dom g ) by A2;
A31: ( f is_integrable_on ['d,b'] & g is_integrable_on ['d,b'] ) by A3, A4, A29, INTEGR10:def 2;
A32: ( f | ['d,b'] is bounded & g | ['d,b'] is bounded ) by A3, A4, A29, INTEGR10:def 2;
then (f + g) | (['d,b'] /\ ['d,b']) is bounded by RFUNCT_1:83;
hence ( f + g is_integrable_on ['d,b'] & (f + g) | ['d,b'] is bounded ) by A30, A31, A32, INTEGRA6:11; :: thesis:

end;

hence A33: f + g is_left_ext_Riemann_integrable_on a,b by A13, A22, A11, A7, LIMFUNC2:54, INTEGR10:def 2; :: thesis:
lim_right ((Intf + Intg),a) = (ext_left_integral (f,a,b)) + (ext_left_integral (g,a,b)) by A11, A12, A7, A8, A22, LIMFUNC2:54;
hence ext_left_integral ((f + g),a,b) = (ext_left_integral (f,a,b)) + (ext_left_integral (g,a,b)) by A13, A28, A33, INTEGR10:def 4; :: thesis: