let f, g be PartFunc of REAL,REAL; :: thesis: for a, b being Real st a < b & ['a,b'] c= dom f & ['a,b'] c= dom g & f is_right_ext_Riemann_integrable_on a,b & g is_right_ext_Riemann_integrable_on a,b holds

( f + g is_right_ext_Riemann_integrable_on a,b & ext_right_integral ((f + g),a,b) = (ext_right_integral (f,a,b)) + (ext_right_integral (g,a,b)) )

let a, b be Real; :: thesis: ( a < b & ['a,b'] c= dom f & ['a,b'] c= dom g & f is_right_ext_Riemann_integrable_on a,b & g is_right_ext_Riemann_integrable_on a,b implies ( f + g is_right_ext_Riemann_integrable_on a,b & ext_right_integral ((f + g),a,b) = (ext_right_integral (f,a,b)) + (ext_right_integral (g,a,b)) ) )

assume that

A1: a < b and

A2: ( ['a,b'] c= dom f & ['a,b'] c= dom g ) and

A3: f is_right_ext_Riemann_integrable_on a,b and

A4: g is_right_ext_Riemann_integrable_on a,b ; :: thesis: ( f + g is_right_ext_Riemann_integrable_on a,b & ext_right_integral ((f + g),a,b) = (ext_right_integral (f,a,b)) + (ext_right_integral (g,a,b)) )

consider Intg being PartFunc of REAL,REAL such that

A5: dom Intg = [.a,b.[ and

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

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

A7: Intg is_left_convergent_in b and

A8: ext_right_integral (g,a,b) = lim_left (Intg,b) by A4, Def3;

consider Intf being PartFunc of REAL,REAL such that

A9: dom Intf = [.a,b.[ and

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

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

A11: Intf is_left_convergent_in b and

A12: ext_right_integral (f,a,b) = lim_left (Intf,b) by A3, Def3;

set Intfg = Intf + Intg;

A13: ( dom (Intf + Intg) = [.a,b.[ & ( for x being Real st x in dom (Intf + Intg) holds

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

ex g being Real st

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

for d being Real st a <= d & d < b holds

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

lim_left ((Intf + Intg),b) = (ext_right_integral (f,a,b)) + (ext_right_integral (g,a,b)) by A11, A12, A7, A8, A23, LIMFUNC2:45;

hence ext_right_integral ((f + g),a,b) = (ext_right_integral (f,a,b)) + (ext_right_integral (g,a,b)) by A13, A30, A36, Def3; :: thesis: verum

( f + g is_right_ext_Riemann_integrable_on a,b & ext_right_integral ((f + g),a,b) = (ext_right_integral (f,a,b)) + (ext_right_integral (g,a,b)) )

let a, b be Real; :: thesis: ( a < b & ['a,b'] c= dom f & ['a,b'] c= dom g & f is_right_ext_Riemann_integrable_on a,b & g is_right_ext_Riemann_integrable_on a,b implies ( f + g is_right_ext_Riemann_integrable_on a,b & ext_right_integral ((f + g),a,b) = (ext_right_integral (f,a,b)) + (ext_right_integral (g,a,b)) ) )

assume that

A1: a < b and

A2: ( ['a,b'] c= dom f & ['a,b'] c= dom g ) and

A3: f is_right_ext_Riemann_integrable_on a,b and

A4: g is_right_ext_Riemann_integrable_on a,b ; :: thesis: ( f + g is_right_ext_Riemann_integrable_on a,b & ext_right_integral ((f + g),a,b) = (ext_right_integral (f,a,b)) + (ext_right_integral (g,a,b)) )

consider Intg being PartFunc of REAL,REAL such that

A5: dom Intg = [.a,b.[ and

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

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

A7: Intg is_left_convergent_in b and

A8: ext_right_integral (g,a,b) = lim_left (Intg,b) by A4, Def3;

consider Intf being PartFunc of REAL,REAL such that

A9: dom Intf = [.a,b.[ and

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

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

A11: Intf is_left_convergent_in b and

A12: ext_right_integral (f,a,b) = lim_left (Intf,b) by A3, Def3;

set Intfg = Intf + Intg;

A13: ( dom (Intf + Intg) = [.a,b.[ & ( for x being Real st x in dom (Intf + Intg) holds

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

proof

A23:
for r being Real st r < b holds
A14:
['a,b'] = [.a,b.]
by A1, INTEGRA5:def 3;

thus A15: dom (Intf + Intg) = (dom Intf) /\ (dom Intg) by VALUED_1:def 1

.= [.a,b.[ by A9, A5 ; :: 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 A16: x in dom (Intf + Intg) ; :: thesis: (Intf + Intg) . x = integral ((f + g),a,x)

then A17: x < b by A15, XXREAL_1:3;

then A18: [.a,x.] c= [.a,b.] by XXREAL_1:34;

A19: a <= x by A15, A16, XXREAL_1:3;

then A20: ( f is_integrable_on ['a,x'] & f | ['a,x'] is bounded ) by A3, A17;

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

then A21: ( ['a,x'] c= dom f & ['a,x'] c= dom g ) by A2, A14, A18;

A22: ( g is_integrable_on ['a,x'] & g | ['a,x'] is bounded ) by A4, A19, A17;

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

.= (integral (f,a,x)) + (Intg . x) by A9, A10, A15, A16

.= (integral (f,a,x)) + (integral (g,a,x)) by A5, A6, A15, A16

.= integral ((f + g),a,x) by A19, A21, A20, A22, INTEGRA6:12 ; :: thesis: verum

end;thus A15: dom (Intf + Intg) = (dom Intf) /\ (dom Intg) by VALUED_1:def 1

.= [.a,b.[ by A9, A5 ; :: 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 A16: x in dom (Intf + Intg) ; :: thesis: (Intf + Intg) . x = integral ((f + g),a,x)

then A17: x < b by A15, XXREAL_1:3;

then A18: [.a,x.] c= [.a,b.] by XXREAL_1:34;

A19: a <= x by A15, A16, XXREAL_1:3;

then A20: ( f is_integrable_on ['a,x'] & f | ['a,x'] is bounded ) by A3, A17;

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

then A21: ( ['a,x'] c= dom f & ['a,x'] c= dom g ) by A2, A14, A18;

A22: ( g is_integrable_on ['a,x'] & g | ['a,x'] is bounded ) by A4, A19, A17;

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

.= (integral (f,a,x)) + (Intg . x) by A9, A10, A15, A16

.= (integral (f,a,x)) + (integral (g,a,x)) by A5, A6, A15, A16

.= integral ((f + g),a,x) by A19, A21, A20, A22, INTEGRA6:12 ; :: thesis: verum

ex g being Real st

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

proof

then A30:
Intf + Intg is_left_convergent_in b
by A11, A7, LIMFUNC2:45;
let r be Real; :: thesis: ( r < b implies ex g being Real st

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

assume A24: r < b ; :: thesis: ex g being Real st

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

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

assume A24: r < b ; :: thesis: ex g being Real st

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

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

end;

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

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

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

reconsider g = a as Real ;

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

thus ( r < g & g < b & g in dom (Intf + Intg) ) by A1, A13, A25, XXREAL_1:3; :: thesis: verum

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

thus ( r < g & g < b & g in dom (Intf + Intg) ) by A1, A13, A25, XXREAL_1:3; :: thesis: verum

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

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

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

then A26:
a - a <= r - a
by XREAL_1:9;

reconsider g = r + ((b - r) / 2) as Real ;

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

A27: 0 < b - r by A24, XREAL_1:50;

then (b - r) / 2 < b - r by XREAL_1:216;

then A28: ((b - r) / 2) + r < (b - r) + r by XREAL_1:8;

r < g by A27, XREAL_1:29, XREAL_1:215;

then A29: r - (r - a) < g - 0 by A26, XREAL_1:14;

0 < (b - r) / 2 by A27, XREAL_1:215;

hence ( r < g & g < b & g in dom (Intf + Intg) ) by A13, A29, A28, XREAL_1:8, XXREAL_1:3; :: thesis: verum

end;reconsider g = r + ((b - r) / 2) as Real ;

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

A27: 0 < b - r by A24, XREAL_1:50;

then (b - r) / 2 < b - r by XREAL_1:216;

then A28: ((b - r) / 2) + r < (b - r) + r by XREAL_1:8;

r < g by A27, XREAL_1:29, XREAL_1:215;

then A29: r - (r - a) < g - 0 by A26, XREAL_1:14;

0 < (b - r) / 2 by A27, XREAL_1:215;

hence ( r < g & g < b & g in dom (Intf + Intg) ) by A13, A29, A28, XREAL_1:8, XXREAL_1:3; :: thesis: verum

for d being Real st a <= d & d < b holds

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

proof

hence A36:
f + g is_right_ext_Riemann_integrable_on a,b
by A13, A30; :: thesis: ext_right_integral ((f + g),a,b) = (ext_right_integral (f,a,b)) + (ext_right_integral (g,a,b))
let d be Real; :: thesis: ( a <= d & d < b implies ( f + g is_integrable_on ['a,d'] & (f + g) | ['a,d'] is bounded ) )

assume A31: ( a <= d & d < b ) ; :: thesis: ( f + g is_integrable_on ['a,d'] & (f + g) | ['a,d'] is bounded )

then A32: ( ['a,d'] = [.a,d.] & [.a,d.] c= [.a,b.] ) by INTEGRA5:def 3, XXREAL_1:34;

['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;

then A33: ( ['a,d'] c= dom f & ['a,d'] c= dom g ) by A2, A32;

A34: ( f is_integrable_on ['a,d'] & g is_integrable_on ['a,d'] ) by A3, A4, A31;

A35: ( f | ['a,d'] is bounded & g | ['a,d'] is bounded ) by A3, A4, A31;

then (f + g) | (['a,d'] /\ ['a,d']) is bounded by RFUNCT_1:83;

hence ( f + g is_integrable_on ['a,d'] & (f + g) | ['a,d'] is bounded ) by A33, A34, A35, INTEGRA6:11; :: thesis: verum

end;assume A31: ( a <= d & d < b ) ; :: thesis: ( f + g is_integrable_on ['a,d'] & (f + g) | ['a,d'] is bounded )

then A32: ( ['a,d'] = [.a,d.] & [.a,d.] c= [.a,b.] ) by INTEGRA5:def 3, XXREAL_1:34;

['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;

then A33: ( ['a,d'] c= dom f & ['a,d'] c= dom g ) by A2, A32;

A34: ( f is_integrable_on ['a,d'] & g is_integrable_on ['a,d'] ) by A3, A4, A31;

A35: ( f | ['a,d'] is bounded & g | ['a,d'] is bounded ) by A3, A4, A31;

then (f + g) | (['a,d'] /\ ['a,d']) is bounded by RFUNCT_1:83;

hence ( f + g is_integrable_on ['a,d'] & (f + g) | ['a,d'] is bounded ) by A33, A34, A35, INTEGRA6:11; :: thesis: verum

lim_left ((Intf + Intg),b) = (ext_right_integral (f,a,b)) + (ext_right_integral (g,a,b)) by A11, A12, A7, A8, A23, LIMFUNC2:45;

hence ext_right_integral ((f + g),a,b) = (ext_right_integral (f,a,b)) + (ext_right_integral (g,a,b)) by A13, A30, A36, Def3; :: thesis: verum