let f, g be PartFunc of REAL,REAL; for a, b being Real st a < b & ].a,b.] c= dom f & ].a,b.] c= dom g & f is_left_ext_Riemann_integrable_on a,b & g is_left_ext_Riemann_integrable_on a,b holds
( f + g is_left_ext_Riemann_integrable_on a,b & ext_left_integral ((f + g),a,b) = (ext_left_integral (f,a,b)) + (ext_left_integral (g,a,b)) )
let a, b be Real; ( a < b & ].a,b.] c= dom f & ].a,b.] c= dom g & f is_left_ext_Riemann_integrable_on a,b & g is_left_ext_Riemann_integrable_on a,b implies ( f + g is_left_ext_Riemann_integrable_on a,b & ext_left_integral ((f + g),a,b) = (ext_left_integral (f,a,b)) + (ext_left_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_left_ext_Riemann_integrable_on a,b
and
A4:
g is_left_ext_Riemann_integrable_on a,b
; ( f + g is_left_ext_Riemann_integrable_on a,b & ext_left_integral ((f + g),a,b) = (ext_left_integral (f,a,b)) + (ext_left_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,x,b)
and
A7:
Intg is_right_convergent_in a
and
A8:
ext_left_integral (g,a,b) = lim_right (Intg,a)
by A4, INTEGR10:def 4;
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,x,b)
and
A11:
Intf is_right_convergent_in a
and
A12:
ext_left_integral (f,a,b) = lim_right (Intf,a)
by A3, INTEGR10:def 4;
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),x,b) ) )
proof
thus A14:
dom (Intf + Intg) =
(dom Intf) /\ (dom Intg)
by VALUED_1:def 1
.=
].a,b.]
by A9, A5
;
for x being Real st x in dom (Intf + Intg) holds
(Intf + Intg) . x = integral ((f + g),x,b)
let x be
Real;
( x in dom (Intf + Intg) implies (Intf + Intg) . x = integral ((f + g),x,b) )
assume A15:
x in dom (Intf + Intg)
;
(Intf + Intg) . x = integral ((f + g),x,b)
then A16:
a < x
by A14, XXREAL_1:2;
then A17:
[.x,b.] c= ].a,b.]
by XXREAL_1:39;
A18:
x <= b
by A14, A15, XXREAL_1:2;
then A19:
(
f is_integrable_on ['x,b'] &
f | ['x,b'] is
bounded )
by A3, A16, INTEGR10:def 2;
['x,b'] = [.x,b.]
by A18, INTEGRA5:def 3;
then A20:
(
['x,b'] c= dom f &
['x,b'] c= dom g )
by A2, A17;
A21:
(
g is_integrable_on ['x,b'] &
g | ['x,b'] is
bounded )
by A4, A16, A18, INTEGR10:def 2;
thus (Intf + Intg) . x =
(Intf . x) + (Intg . x)
by A15, VALUED_1:def 1
.=
(integral (f,x,b)) + (Intg . x)
by A9, A10, A14, A15
.=
(integral (f,x,b)) + (integral (g,x,b))
by A5, A6, A14, A15
.=
integral (
(f + g),
x,
b)
by A18, A20, A19, A21, INTEGRA6:12
;
verum
end;
A22:
for r being Real st a < r holds
ex g being Real st
( g < r & a < g & g in dom (Intf + Intg) )
proof
let r be
Real;
( a < r implies ex g being Real st
( g < r & a < g & g in dom (Intf + Intg) ) )
assume A23:
a < r
;
ex g being Real st
( g < r & a < g & g in dom (Intf + Intg) )
end;
then A28:
Intf + Intg is_right_convergent_in a
by A11, A7, LIMFUNC2:54;
for d being Real st a < d & d <= b holds
( f + g is_integrable_on ['d,b'] & (f + g) | ['d,b'] is bounded )
proof
let d be
Real;
( a < d & d <= b implies ( f + g is_integrable_on ['d,b'] & (f + g) | ['d,b'] is bounded ) )
assume A29:
(
a < d &
d <= b )
;
( f + g is_integrable_on ['d,b'] & (f + g) | ['d,b'] is bounded )
then
(
['d,b'] = [.d,b.] &
[.d,b.] c= ].a,b.] )
by INTEGRA5:def 3, XXREAL_1:39;
then A30:
(
['d,b'] c= dom f &
['d,b'] c= dom g )
by A2;
A31:
(
f is_integrable_on ['d,b'] &
g is_integrable_on ['d,b'] )
by A3, A4, A29, INTEGR10:def 2;
A32:
(
f | ['d,b'] is
bounded &
g | ['d,b'] is
bounded )
by A3, A4, A29, INTEGR10:def 2;
then
(f + g) | (['d,b'] /\ ['d,b']) is
bounded
by RFUNCT_1:83;
hence
(
f + g is_integrable_on ['d,b'] &
(f + g) | ['d,b'] is
bounded )
by A30, A31, A32, INTEGRA6:11;
verum
end;
hence A33:
f + g is_left_ext_Riemann_integrable_on a,b
by A13, A22, A11, A7, LIMFUNC2:54, INTEGR10:def 2; ext_left_integral ((f + g),a,b) = (ext_left_integral (f,a,b)) + (ext_left_integral (g,a,b))
lim_right ((Intf + Intg),a) = (ext_left_integral (f,a,b)) + (ext_left_integral (g,a,b))
by A11, A12, A7, A8, A22, LIMFUNC2:54;
hence
ext_left_integral ((f + g),a,b) = (ext_left_integral (f,a,b)) + (ext_left_integral (g,a,b))
by A13, A28, A33, INTEGR10:def 4; verum