let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st ex A being Element of S st
( A = dom f & A = dom g & f is A -measurable & g is A -measurable ) & f is nonnegative & g is nonnegative holds
integral+ (M,(f + g)) = (integral+ (M,f)) + (integral+ (M,g))
let S be SigmaField of X; for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st ex A being Element of S st
( A = dom f & A = dom g & f is A -measurable & g is A -measurable ) & f is nonnegative & g is nonnegative holds
integral+ (M,(f + g)) = (integral+ (M,f)) + (integral+ (M,g))
let M be sigma_Measure of S; for f, g being PartFunc of X,ExtREAL st ex A being Element of S st
( A = dom f & A = dom g & f is A -measurable & g is A -measurable ) & f is nonnegative & g is nonnegative holds
integral+ (M,(f + g)) = (integral+ (M,f)) + (integral+ (M,g))
let f, g be PartFunc of X,ExtREAL; ( ex A being Element of S st
( A = dom f & A = dom g & f is A -measurable & g is A -measurable ) & f is nonnegative & g is nonnegative implies integral+ (M,(f + g)) = (integral+ (M,f)) + (integral+ (M,g)) )
assume that
A1:
ex A being Element of S st
( A = dom f & A = dom g & f is A -measurable & g is A -measurable )
and
A2:
f is nonnegative
and
A3:
g is nonnegative
; integral+ (M,(f + g)) = (integral+ (M,f)) + (integral+ (M,g))
consider F1 being Functional_Sequence of X,ExtREAL, K1 being ExtREAL_sequence such that
A4:
for n being Nat holds
( F1 . n is_simple_func_in S & dom (F1 . n) = dom f )
and
A5:
for n being Nat holds F1 . n is nonnegative
and
A6:
for n, m being Nat st n <= m holds
for x being Element of X st x in dom f holds
(F1 . n) . x <= (F1 . m) . x
and
A7:
for x being Element of X st x in dom f holds
( F1 # x is convergent & lim (F1 # x) = f . x )
and
A8:
for n being Nat holds K1 . n = integral' (M,(F1 . n))
and
K1 is convergent
and
A9:
integral+ (M,f) = lim K1
by A1, A2, Def15;
A10:
f + g is nonnegative
by A2, A3, Th19;
consider A being Element of S such that
A11:
A = dom f
and
A12:
A = dom g
and
A13:
f is A -measurable
and
A14:
g is A -measurable
by A1;
A = (dom f) /\ (dom g)
by A11, A12;
then A15:
A = dom (f + g)
by A2, A3, Th16;
A16:
for n, m being Nat st n <= m holds
K1 . n <= K1 . m
proof
let n,
m be
Nat;
( n <= m implies K1 . n <= K1 . m )
assume A17:
n <= m
;
K1 . n <= K1 . m
A18:
dom (F1 . m) = dom f
by A4;
A19:
dom (F1 . n) = dom f
by A4;
A21:
F1 . m is
nonnegative
by A5;
A22:
F1 . n is
nonnegative
by A5;
A23:
K1 . m = integral' (
M,
(F1 . m))
by A8;
A24:
K1 . n = integral' (
M,
(F1 . n))
by A8;
A25:
F1 . m is_simple_func_in S
by A4;
A26:
F1 . n is_simple_func_in S
by A4;
then A27:
dom ((F1 . m) - (F1 . n)) = (dom (F1 . m)) /\ (dom (F1 . n))
by A25, A22, A21, A20, Th69;
then A28:
(F1 . m) | (dom ((F1 . m) - (F1 . n))) = F1 . m
by A19, A18, GRFUNC_1:23;
(F1 . n) | (dom ((F1 . m) - (F1 . n))) = F1 . n
by A19, A18, A27, GRFUNC_1:23;
hence
K1 . n <= K1 . m
by A24, A23, A26, A25, A22, A21, A20, A28, Th70;
verum
end;
consider F2 being Functional_Sequence of X,ExtREAL, K2 being ExtREAL_sequence such that
A29:
for n being Nat holds
( F2 . n is_simple_func_in S & dom (F2 . n) = dom g )
and
A30:
for n being Nat holds F2 . n is nonnegative
and
A31:
for n, m being Nat st n <= m holds
for x being Element of X st x in dom g holds
(F2 . n) . x <= (F2 . m) . x
and
A32:
for x being Element of X st x in dom g holds
( F2 # x is convergent & lim (F2 # x) = g . x )
and
A33:
for n being Nat holds K2 . n = integral' (M,(F2 . n))
and
K2 is convergent
and
A34:
integral+ (M,g) = lim K2
by A1, A3, Def15;
deffunc H1( Nat) -> Element of bool [:X,ExtREAL:] = (F1 . $1) + (F2 . $1);
consider F being Functional_Sequence of X,ExtREAL such that
A35:
for n being Nat holds F . n = H1(n)
from SEQFUNC:sch 1();
A36:
for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom (f + g) & F . n is nonnegative )
proof
let n be
Nat;
( F . n is_simple_func_in S & dom (F . n) = dom (f + g) & F . n is nonnegative )
A37:
dom (F1 . n) = dom f
by A4;
A38:
F2 . n is_simple_func_in S
by A29;
A39:
F2 . n is
nonnegative
by A30;
A40:
F . n = (F1 . n) + (F2 . n)
by A35;
A41:
F1 . n is_simple_func_in S
by A4;
hence
F . n is_simple_func_in S
by A38, A40, Th38;
( dom (F . n) = dom (f + g) & F . n is nonnegative )
A42:
dom (F2 . n) = dom g
by A29;
F1 . n is
nonnegative
by A5;
then
dom (F . n) = (dom (F1 . n)) /\ (dom (F2 . n))
by A41, A38, A39, A40, Th65;
hence
dom (F . n) = dom (f + g)
by A2, A3, A37, A42, Th16;
F . n is nonnegative
A43:
F2 . n is
nonnegative
by A30;
A44:
F . n = (F1 . n) + (F2 . n)
by A35;
F1 . n is
nonnegative
by A5;
hence
F . n is
nonnegative
by A43, A44, Th19;
verum
end;
A45:
for n, m being Nat st n <= m holds
for x being Element of X st x in dom (f + g) holds
(F . n) . x <= (F . m) . x
proof
let n,
m be
Nat;
( n <= m implies for x being Element of X st x in dom (f + g) holds
(F . n) . x <= (F . m) . x )
assume A46:
n <= m
;
for x being Element of X st x in dom (f + g) holds
(F . n) . x <= (F . m) . x
dom ((F1 . m) + (F2 . m)) = dom (F . m)
by A35;
then A47:
dom ((F1 . m) + (F2 . m)) = dom (f + g)
by A36;
dom ((F1 . n) + (F2 . n)) = dom (F . n)
by A35;
then A48:
dom ((F1 . n) + (F2 . n)) = dom (f + g)
by A36;
let x be
Element of
X;
( x in dom (f + g) implies (F . n) . x <= (F . m) . x )
assume A49:
x in dom (f + g)
;
(F . n) . x <= (F . m) . x
then A50:
(F2 . n) . x <= (F2 . m) . x
by A31, A12, A15, A46;
(F . m) . x = ((F1 . m) + (F2 . m)) . x
by A35;
then A51:
(F . m) . x = ((F1 . m) . x) + ((F2 . m) . x)
by A49, A47, MESFUNC1:def 3;
(F . n) . x = ((F1 . n) + (F2 . n)) . x
by A35;
then A52:
(F . n) . x = ((F1 . n) . x) + ((F2 . n) . x)
by A49, A48, MESFUNC1:def 3;
(F1 . n) . x <= (F1 . m) . x
by A6, A11, A15, A46, A49;
hence
(F . n) . x <= (F . m) . x
by A52, A51, A50, XXREAL_3:36;
verum
end;
then A54:
K2 is ()
by Th10;
deffunc H2( Nat) -> Element of ExtREAL = integral' (M,(F . $1));
consider K being ExtREAL_sequence such that
A55:
for n being Element of NAT holds K . n = H2(n)
from FUNCT_2:sch 4();
A56:
now for n being Nat holds K . n = H2(n)end;
A57:
for n being Nat holds K . n = (K1 . n) + (K2 . n)
proof
let n be
Nat;
K . n = (K1 . n) + (K2 . n)
A58:
F1 . n is
nonnegative
by A5;
A59:
F . n = (F1 . n) + (F2 . n)
by A35;
A60:
dom (F1 . n) =
dom f
by A4
.=
dom (F2 . n)
by A29, A11, A12
;
A61:
F2 . n is_simple_func_in S
by A29;
A62:
K . n = integral' (
M,
(F . n))
by A56;
A63:
F2 . n is
nonnegative
by A30;
A64:
F1 . n is_simple_func_in S
by A4;
then
dom (F . n) = (dom (F1 . n)) /\ (dom (F2 . n))
by A58, A61, A63, A59, Th65;
then
K . n = (integral' (M,((F1 . n) | (dom (F1 . n))))) + (integral' (M,((F2 . n) | (dom (F2 . n)))))
by A64, A58, A61, A63, A59, A60, A62, Th65;
then
K . n = (integral' (M,(F1 . n))) + (integral' (M,((F2 . n) | (dom (F2 . n)))))
by GRFUNC_1:23;
then A65:
K . n = (integral' (M,(F1 . n))) + (integral' (M,(F2 . n)))
by GRFUNC_1:23;
K2 . n = integral' (
M,
(F2 . n))
by A33;
hence
K . n = (K1 . n) + (K2 . n)
by A8, A65;
verum
end;
A66:
for n, m being Nat st n <= m holds
K2 . n <= K2 . m
proof
let n,
m be
Nat;
( n <= m implies K2 . n <= K2 . m )
assume A67:
n <= m
;
K2 . n <= K2 . m
A68:
dom (F2 . m) = dom g
by A29;
A69:
dom (F2 . n) = dom g
by A29;
A71:
F2 . m is
nonnegative
by A30;
A72:
F2 . n is
nonnegative
by A30;
A73:
K2 . m = integral' (
M,
(F2 . m))
by A33;
A74:
K2 . n = integral' (
M,
(F2 . n))
by A33;
A75:
F2 . m is_simple_func_in S
by A29;
A76:
F2 . n is_simple_func_in S
by A29;
then A77:
dom ((F2 . m) - (F2 . n)) = (dom (F2 . m)) /\ (dom (F2 . n))
by A75, A72, A71, A70, Th69;
then A78:
(F2 . m) | (dom ((F2 . m) - (F2 . n))) = F2 . m
by A69, A68, GRFUNC_1:23;
(F2 . n) | (dom ((F2 . m) - (F2 . n))) = F2 . n
by A69, A68, A77, GRFUNC_1:23;
hence
K2 . n <= K2 . m
by A74, A73, A76, A75, A72, A71, A70, A78, Th70;
verum
end;
then A80:
K1 is ()
by Th10;
then A81:
lim K = (lim K1) + (lim K2)
by A16, A54, A66, A57, Th61;
A82:
for x being Element of X st x in dom (f + g) holds
( F # x is convergent & lim (F # x) = (f + g) . x )
proof
let x be
Element of
X;
( x in dom (f + g) implies ( F # x is convergent & lim (F # x) = (f + g) . x ) )
then A86:
F2 # x is ()
by Th10;
assume A87:
x in dom (f + g)
;
( F # x is convergent & lim (F # x) = (f + g) . x )
then
(lim (F1 # x)) + (lim (F2 # x)) = (f . x) + (lim (F2 # x))
by A7, A11, A15;
then
(lim (F1 # x)) + (lim (F2 # x)) = (f . x) + (g . x)
by A32, A12, A15, A87;
then A88:
(lim (F1 # x)) + (lim (F2 # x)) = (f + g) . x
by A87, MESFUNC1:def 3;
A89:
now for n, m being Nat st n <= m holds
(F2 # x) . n <= (F2 # x) . mend;
A92:
now for n, m being Nat st n <= m holds
(F1 # x) . n <= (F1 # x) . mend;
A95:
now for n being Nat holds (F # x) . n = ((F1 # x) . n) + ((F2 # x) . n)end;
F1 # x is ()
by A83, Th10;
hence
(
F # x is
convergent &
lim (F # x) = (f + g) . x )
by A95, A86, A92, A89, A88, Th61;
verum
end;
A97:
f + g is A -measurable
by A2, A3, A13, A14, Th31;
K is convergent
by A80, A16, A54, A66, A57, Th61;
hence
integral+ (M,(f + g)) = (integral+ (M,f)) + (integral+ (M,g))
by A9, A34, A97, A15, A10, A56, A36, A45, A82, A81, Def15; verum