let f, g be PartFunc of REAL,REAL; :: thesis: for a being Real st 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 holds

( f + g is_+infty_ext_Riemann_integrable_on a & infty_ext_right_integral ((f + g),a) = (infty_ext_right_integral (f,a)) + (infty_ext_right_integral (g,a)) )

let a be Real; :: thesis: ( 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 implies ( f + g is_+infty_ext_Riemann_integrable_on a & infty_ext_right_integral ((f + g),a) = (infty_ext_right_integral (f,a)) + (infty_ext_right_integral (g,a)) ) )

assume that

A1: ( right_closed_halfline a c= dom f & right_closed_halfline a c= dom g ) and

A2: f is_+infty_ext_Riemann_integrable_on a and

A3: g is_+infty_ext_Riemann_integrable_on a ; :: thesis: ( f + g is_+infty_ext_Riemann_integrable_on a & infty_ext_right_integral ((f + g),a) = (infty_ext_right_integral (f,a)) + (infty_ext_right_integral (g,a)) )

consider Intg being PartFunc of REAL,REAL such that

A4: dom Intg = right_closed_halfline a and

A5: for x being Real st x in dom Intg holds

Intg . x = integral (g,a,x) and

A6: Intg is convergent_in+infty and

A7: infty_ext_right_integral (g,a) = lim_in+infty Intg by A3, Def7;

consider Intf being PartFunc of REAL,REAL such that

A8: dom Intf = right_closed_halfline a and

A9: for x being Real st x in dom Intf holds

Intf . x = integral (f,a,x) and

A10: Intf is convergent_in+infty and

A11: infty_ext_right_integral (f,a) = lim_in+infty Intf by A2, Def7;

set Intfg = Intf + Intg;

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

( r < g & g in dom (Intf + Intg) )

for b being Real st a <= b holds

( f + g is_integrable_on ['a,b'] & (f + g) | ['a,b'] is bounded )

lim_in+infty (Intf + Intg) = (infty_ext_right_integral (f,a)) + (infty_ext_right_integral (g,a)) by A10, A11, A6, A7, A20, LIMFUNC1:82;

hence infty_ext_right_integral ((f + g),a) = (infty_ext_right_integral (f,a)) + (infty_ext_right_integral (g,a)) by A12, A24, A30, Def7; :: thesis: verum

( f + g is_+infty_ext_Riemann_integrable_on a & infty_ext_right_integral ((f + g),a) = (infty_ext_right_integral (f,a)) + (infty_ext_right_integral (g,a)) )

let a be Real; :: thesis: ( 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 implies ( f + g is_+infty_ext_Riemann_integrable_on a & infty_ext_right_integral ((f + g),a) = (infty_ext_right_integral (f,a)) + (infty_ext_right_integral (g,a)) ) )

assume that

A1: ( right_closed_halfline a c= dom f & right_closed_halfline a c= dom g ) and

A2: f is_+infty_ext_Riemann_integrable_on a and

A3: g is_+infty_ext_Riemann_integrable_on a ; :: thesis: ( f + g is_+infty_ext_Riemann_integrable_on a & infty_ext_right_integral ((f + g),a) = (infty_ext_right_integral (f,a)) + (infty_ext_right_integral (g,a)) )

consider Intg being PartFunc of REAL,REAL such that

A4: dom Intg = right_closed_halfline a and

A5: for x being Real st x in dom Intg holds

Intg . x = integral (g,a,x) and

A6: Intg is convergent_in+infty and

A7: infty_ext_right_integral (g,a) = lim_in+infty Intg by A3, Def7;

consider Intf being PartFunc of REAL,REAL such that

A8: dom Intf = right_closed_halfline a and

A9: for x being Real st x in dom Intf holds

Intf . x = integral (f,a,x) and

A10: Intf is convergent_in+infty and

A11: infty_ext_right_integral (f,a) = lim_in+infty Intf by A2, Def7;

set Intfg = Intf + Intg;

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

A20:
for r being Real ex g being Real st
thus A13: dom (Intf + Intg) =
(dom Intf) /\ (dom Intg)
by VALUED_1:def 1

.= right_closed_halfline a by A8, A4 ; :: thesis: for x being Real st x in dom (Intf + Intg) holds

(Intf + Intg) . x = integral ((f + g),a,x)

let x be Real; :: thesis: ( x in dom (Intf + Intg) implies (Intf + Intg) . x = integral ((f + g),a,x) )

assume A14: x in dom (Intf + Intg) ; :: thesis: (Intf + Intg) . x = integral ((f + g),a,x)

then A15: a <= x by A13, XXREAL_1:236;

then A16: ( f is_integrable_on ['a,x'] & f | ['a,x'] is bounded ) by A2;

A17: [.a,x.] c= right_closed_halfline a by XXREAL_1:251;

['a,x'] = [.a,x.] by A15, INTEGRA5:def 3;

then A18: ( ['a,x'] c= dom f & ['a,x'] c= dom g ) by A1, A17;

A19: ( g is_integrable_on ['a,x'] & g | ['a,x'] is bounded ) by A3, A15;

thus (Intf + Intg) . x = (Intf . x) + (Intg . x) by A14, VALUED_1:def 1

.= (integral (f,a,x)) + (Intg . x) by A8, A9, A13, A14

.= (integral (f,a,x)) + (integral (g,a,x)) by A4, A5, A13, A14

.= integral ((f + g),a,x) by A15, A18, A16, A19, INTEGRA6:12 ; :: thesis: verum

end;.= right_closed_halfline a by A8, A4 ; :: thesis: for x being Real st x in dom (Intf + Intg) holds

(Intf + Intg) . x = integral ((f + g),a,x)

let x be Real; :: thesis: ( x in dom (Intf + Intg) implies (Intf + Intg) . x = integral ((f + g),a,x) )

assume A14: x in dom (Intf + Intg) ; :: thesis: (Intf + Intg) . x = integral ((f + g),a,x)

then A15: a <= x by A13, XXREAL_1:236;

then A16: ( f is_integrable_on ['a,x'] & f | ['a,x'] is bounded ) by A2;

A17: [.a,x.] c= right_closed_halfline a by XXREAL_1:251;

['a,x'] = [.a,x.] by A15, INTEGRA5:def 3;

then A18: ( ['a,x'] c= dom f & ['a,x'] c= dom g ) by A1, A17;

A19: ( g is_integrable_on ['a,x'] & g | ['a,x'] is bounded ) by A3, A15;

thus (Intf + Intg) . x = (Intf . x) + (Intg . x) by A14, VALUED_1:def 1

.= (integral (f,a,x)) + (Intg . x) by A8, A9, A13, A14

.= (integral (f,a,x)) + (integral (g,a,x)) by A4, A5, A13, A14

.= integral ((f + g),a,x) by A15, A18, A16, A19, INTEGRA6:12 ; :: thesis: verum

( r < g & g in dom (Intf + Intg) )

proof

then A24:
Intf + Intg is convergent_in+infty
by A10, A6, LIMFUNC1:82;
let r be Real; :: thesis: ex g being Real st

( r < g & g in dom (Intf + Intg) )

end;( r < g & g in dom (Intf + Intg) )

per cases
( r < a or not r < a )
;

end;

suppose A21:
r < a
; :: thesis: ex g being Real st

( r < g & g in dom (Intf + Intg) )

( r < g & g in dom (Intf + Intg) )

reconsider g = a as Real ;

take g ; :: thesis: ( r < g & g in dom (Intf + Intg) )

thus ( r < g & g in dom (Intf + Intg) ) by A12, A21, XXREAL_1:236; :: thesis: verum

end;take g ; :: thesis: ( r < g & g in dom (Intf + Intg) )

thus ( r < g & g in dom (Intf + Intg) ) by A12, A21, XXREAL_1:236; :: thesis: verum

suppose A22:
not r < a
; :: thesis: ex g being Real st

( r < g & g in dom (Intf + Intg) )

( r < g & g in dom (Intf + Intg) )

reconsider g = r + 1 as Real ;

take g ; :: thesis: ( r < g & g in dom (Intf + Intg) )

A23: r + 0 < r + 1 by XREAL_1:8;

then a <= g by A22, XXREAL_0:2;

hence ( r < g & g in dom (Intf + Intg) ) by A12, A23, XXREAL_1:236; :: thesis: verum

end;take g ; :: thesis: ( r < g & g in dom (Intf + Intg) )

A23: r + 0 < r + 1 by XREAL_1:8;

then a <= g by A22, XXREAL_0:2;

hence ( r < g & g in dom (Intf + Intg) ) by A12, A23, XXREAL_1:236; :: thesis: verum

for b being Real st a <= b holds

( f + g is_integrable_on ['a,b'] & (f + g) | ['a,b'] is bounded )

proof

hence A30:
f + g is_+infty_ext_Riemann_integrable_on a
by A12, A24; :: thesis: infty_ext_right_integral ((f + g),a) = (infty_ext_right_integral (f,a)) + (infty_ext_right_integral (g,a))
let b be Real; :: thesis: ( a <= b implies ( f + g is_integrable_on ['a,b'] & (f + g) | ['a,b'] is bounded ) )

A25: [.a,b.] c= right_closed_halfline a by XXREAL_1:251;

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 A26, INTEGRA5:def 3;

then A28: ( ['a,b'] c= dom f & ['a,b'] c= dom g ) by A1, A25;

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 A28, A27, A29, INTEGRA6:11; :: thesis: verum

end;A25: [.a,b.] c= right_closed_halfline a by XXREAL_1:251;

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 A26, INTEGRA5:def 3;

then A28: ( ['a,b'] c= dom f & ['a,b'] c= dom g ) by A1, A25;

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 A28, A27, A29, INTEGRA6:11; :: thesis: verum

lim_in+infty (Intf + Intg) = (infty_ext_right_integral (f,a)) + (infty_ext_right_integral (g,a)) by A10, A11, A6, A7, A20, LIMFUNC1:82;

hence infty_ext_right_integral ((f + g),a) = (infty_ext_right_integral (f,a)) + (infty_ext_right_integral (g,a)) by A12, A24, A30, Def7; :: thesis: verum