let f, g be PartFunc of REAL,REAL; :: thesis: for b being Real st 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 holds
( f + g is_-infty_ext_Riemann_integrable_on b & infty_ext_left_integral ((f + g),b) = () + () )

let b be Real; :: thesis:
assume that
A1: ( left_closed_halfline b c= dom f & left_closed_halfline b c= dom g ) and
A2: f is_-infty_ext_Riemann_integrable_on b and
A3: g is_-infty_ext_Riemann_integrable_on b ; :: thesis: ( f + g is_-infty_ext_Riemann_integrable_on b & infty_ext_left_integral ((f + g),b) = () + () )
consider Intg being PartFunc of REAL,REAL such that
A4: dom Intg = left_closed_halfline b and
A5: for x being Real st x in dom Intg holds
Intg . x = integral (g,x,b) and
A6: Intg is convergent_in-infty and
A7: infty_ext_left_integral (g,b) = lim_in-infty Intg by ;
consider Intf being PartFunc of REAL,REAL such that
A8: dom Intf = left_closed_halfline b and
A9: for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) and
A10: Intf is convergent_in-infty and
A11: infty_ext_left_integral (f,b) = lim_in-infty Intf by ;
set Intfg = Intf + Intg;
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 A8, A4 ; :: thesis: for x being Real st x in dom (Intf + Intg) holds
(Intf + Intg) . x = integral ((f + g),x,b)

let x be Real; :: thesis: ( x in dom (Intf + Intg) implies (Intf + Intg) . x = integral ((f + g),x,b) )
assume A14: x in dom (Intf + Intg) ; :: thesis: (Intf + Intg) . x = integral ((f + g),x,b)
then A15: x <= b by ;
then A16: ( f is_integrable_on ['x,b'] & f | ['x,b'] is bounded ) by A2;
A17: [.x,b.] c= left_closed_halfline b by XXREAL_1:265;
['x,b'] = [.x,b.] by ;
then A18: ( ['x,b'] c= dom f & ['x,b'] c= dom g ) by ;
A19: ( g is_integrable_on ['x,b'] & g | ['x,b'] is bounded ) by ;
thus (Intf + Intg) . x = (Intf . x) + (Intg . x) by
.= (integral (f,x,b)) + (Intg . x) by A8, A9, A13, A14
.= (integral (f,x,b)) + (integral (g,x,b)) by A4, A5, A13, A14
.= integral ((f + g),x,b) by ; :: thesis: verum
end;
A20: for r being Real ex g being Real st
( g < r & g in dom (Intf + Intg) )
proof
let r be Real; :: thesis: ex g being Real st
( g < r & g in dom (Intf + Intg) )

per cases ( b < r or not b < r ) ;
suppose A21: b < r ; :: thesis: ex g being Real st
( g < r & g in dom (Intf + Intg) )

reconsider g = b as Real ;
take g ; :: thesis: ( g < r & g in dom (Intf + Intg) )
thus ( g < r & g in dom (Intf + Intg) ) by ; :: thesis: verum
end;
suppose A22: not b < r ; :: thesis: ex g being Real st
( g < r & g in dom (Intf + Intg) )

reconsider g = r - 1 as Real ;
take g ; :: thesis: ( g < r & g in dom (Intf + Intg) )
A23: r - 1 < r - 0 by XREAL_1:15;
then g <= b by ;
hence ( g < r & g in dom (Intf + Intg) ) by ; :: thesis: verum
end;
end;
end;
then A24: Intf + Intg is convergent_in-infty by ;
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: ( a <= b implies ( f + g is_integrable_on ['a,b'] & (f + g) | ['a,b'] is bounded ) )
A25: [.a,b.] c= left_closed_halfline b by XXREAL_1:265;
assume A26: a <= b ; :: thesis: ( f + g is_integrable_on ['a,b'] & (f + g) | ['a,b'] is bounded )
then A27: ( f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] ) by A2, A3;
['a,b'] = [.a,b.] by ;
then A28: ( ['a,b'] c= dom f & ['a,b'] c= dom g ) by ;
A29: ( f | ['a,b'] is bounded & g | ['a,b'] is bounded ) by A2, A3, A26;
then (f + g) | (['a,b'] /\ ['a,b']) is bounded by RFUNCT_1:83;
hence ( f + g is_integrable_on ['a,b'] & (f + g) | ['a,b'] is bounded ) by ; :: thesis: verum
end;
hence A30: f + g is_-infty_ext_Riemann_integrable_on b by ; :: thesis: infty_ext_left_integral ((f + g),b) = () + ()
lim_in-infty (Intf + Intg) = () + () by ;
hence infty_ext_left_integral ((f + g),b) = () + () by ; :: thesis: verum