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

proof

let b be Real; :: thesis:
assume A5: a <= b ; :: thesis:
A6: ['a,b'] = [.a,b.] by INTEGRA5:def 4, A5;
A7: [.a,b.] c= right_closed_halfline a by XXREAL_1:251;
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, Def5, A1;
A11: ( g is_integrable_on ['a,b'] & g | ['a,b'] is bounded ) by A5, Def5, 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) = right_closed_halfline a & ( for x being Real st x in dom (Intf + Intg) holds
(Intf + Intg) . x = integral (f + g),a,x ) )

proof

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

end;

A22: ( Intf + Intg is convergent_in+infty & lim_in+infty (Intf + Intg) = (infty_ext_right_integral f,a) + (infty_ext_right_integral g,a) )

proof

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

proof

let r be Real; :: thesis:

per cases ;

suppose A24: r < a ; :: thesis:

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

end;

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

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

end;

thus Intf + Intg is convergent_in+infty by LIMFUNC1:117, A2, A3, A23; :: thesis:
thus lim_in+infty (Intf + Intg) = (infty_ext_right_integral f,a) + (infty_ext_right_integral g,a) by LIMFUNC1:117, A2, A3, A23; :: thesis:

end;

thus f + g is_+infty_ext_Riemann_integrable_on a by A4, A12, A22, Def5; :: thesis:
hence infty_ext_right_integral (f + g),a = (infty_ext_right_integral f,a) + (infty_ext_right_integral g,a) by A12, A22, Def7; :: thesis: