let f, g be PartFunc of REAL ,REAL ; :: thesis:
let b be real number ; :: thesis:
assume A1: ( left_closed_halfline b c= dom f & left_closed_halfline b c= dom g & f is_-infty_ext_Riemann_integrable_on b & g is_-infty_ext_Riemann_integrable_on b ) ; :: thesis:
consider Intf being PartFunc of REAL ,REAL such that
A2: ( dom Intf = left_closed_halfline b & ( for x being Real st x in dom Intf holds
Intf . x = integral f,x,b ) & Intf is convergent_in-infty & infty_ext_left_integral f,b = lim_in-infty Intf ) by Def8, A1;
consider Intg being PartFunc of REAL ,REAL such that
A3: ( dom Intg = left_closed_halfline b & ( for x being Real st x in dom Intg holds
Intg . x = integral g,x,b ) & Intg is convergent_in-infty & infty_ext_left_integral g,b = lim_in-infty Intg ) by Def8, A1;
set Intfg = Intf + Intg;
A4: for a being Real st a <= b holds
( f + g is_integrable_on ['a,b'] & (f + g) | ['a,b'] is bounded )

proof

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

end;

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

proof

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

end;

A22: ( Intf + Intg is convergent_in-infty & lim_in-infty (Intf + Intg) = (infty_ext_left_integral f,b) + (infty_ext_left_integral g,b) )

proof

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

proof

let r be Real; :: thesis:

per cases ;

suppose A24: b < r ; :: thesis:

reconsider g = b as Real by XREAL_0:def 1;
take g ; :: thesis:
thus ( g < r & g in dom (Intf + Intg) ) by A24, A12, XXREAL_1:234; :: thesis:

end;

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

reconsider g = r - 1 as Real ;
take g ; :: thesis:
A26: r - 1 < r - 0 by XREAL_1:17;
g <= b by A25, A26, XXREAL_0:2;
hence ( g < r & g in dom (Intf + Intg) ) by A26, A12, XXREAL_1:234; :: thesis:

end;

thus Intf + Intg is convergent_in-infty by LIMFUNC1:126, A2, A3, A23; :: thesis:
thus lim_in-infty (Intf + Intg) = (infty_ext_left_integral f,b) + (infty_ext_left_integral g,b) by LIMFUNC1:126, A2, A3, A23; :: thesis:

end;

thus f + g is_-infty_ext_Riemann_integrable_on b by A4, A12, A22, Def6; :: thesis:
hence infty_ext_left_integral (f + g),b = (infty_ext_left_integral f,b) + (infty_ext_left_integral g,b) by A12, A22, Def8; :: thesis: