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_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; ( 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
; ( 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
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
;
for x being Real st x in dom (Intf + Intg) holds
(Intf + Intg) . x = integral ((f + g),a,x)
let x be
Real;
( x in dom (Intf + Intg) implies (Intf + Intg) . x = integral ((f + g),a,x) )
assume A16:
x in dom (Intf + Intg)
;
(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
;
verum
end;
A23:
for r being Real st r < b holds
ex g being Real st
( r < g & g < b & g in dom (Intf + Intg) )
proof
let r be
Real;
( r < b implies ex g being Real st
( r < g & g < b & g in dom (Intf + Intg) ) )
assume A24:
r < b
;
ex g being Real st
( r < g & g < b & g in dom (Intf + Intg) )
end;
then A30:
Intf + Intg is_left_convergent_in b
by A11, A7, LIMFUNC2:45;
for d being Real st a <= d & d < b holds
( f + g is_integrable_on ['a,d'] & (f + g) | ['a,d'] is bounded )
proof
let d be
Real;
( a <= d & d < b implies ( f + g is_integrable_on ['a,d'] & (f + g) | ['a,d'] is bounded ) )
assume A31:
(
a <= d &
d < b )
;
( 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;
verum
end;
hence A36:
f + g is_right_ext_Riemann_integrable_on a,b
by A13, A30; ext_right_integral ((f + g),a,b) = (ext_right_integral (f,a,b)) + (ext_right_integral (g,a,b))
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; verum