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_left_ext_Riemann_integrable_on a,b & g is_left_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,x,b ) & Intf is_right_convergent_in a & ext_left_integral f,a,b = lim_right Intf,a ) by Def4, 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,x,b ) & Intg is_right_convergent_in a & ext_left_integral g,a,b = lim_right Intg,a ) by Def4, A1;
set Intfg = Intf + Intg;
A4: for d being Real st a < d & d <= b holds
( f + g is_integrable_on ['d,b'] & (f + g) | ['d,b'] is bounded )

proof

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

end;

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 ) )

proof

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

end;

A24: ( Intf + Intg is_right_convergent_in a & lim_right (Intf + Intg),a = (ext_left_integral f,a,b) + (ext_left_integral g,a,b) )

proof

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

proof

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

per cases ;

suppose A27: b < r ; :: thesis:

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

end;

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

reconsider g = r - ((r - a) / 2) as Real ;
take g ; :: thesis:
0 < r - a by A26, XREAL_1:52;
then A29: ( 0 < (r - a) / 2 & (r - a) / 2 < r - a ) by XREAL_1:217, XREAL_1:218;
A30: ((r - a) / 2) + (a - ((r - a) / 2)) < (r - a) + (a - ((r - a) / 2)) by A29, XREAL_1:10;
r - ((r - a) / 2) < b - 0 by A28, A29, XREAL_1:17;
hence ( g < r & a < g & g in dom (Intf + Intg) ) by XXREAL_1:2, XREAL_1:46, A13, A30, A29; :: thesis:

end;

thus Intf + Intg is_right_convergent_in a by LIMFUNC2:62, A2, A3, A25; :: thesis:
thus lim_right (Intf + Intg),a = (ext_left_integral f,a,b) + (ext_left_integral g,a,b) by LIMFUNC2:62, A2, A3, A25; :: thesis:

end;

thus f + g is_left_ext_Riemann_integrable_on a,b by A4, A13, A24, Def2; :: thesis:
hence ext_left_integral (f + g),a,b = (ext_left_integral f,a,b) + (ext_left_integral g,a,b) by A13, A24, Def4; :: thesis: