let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A, B being Element of S st ex E being Element of S st
( E = dom f & f is E -measurable ) & f is nonnegative & A misses B holds
integral+ (M,(f | (A \/ B))) = (integral+ (M,(f | A))) + (integral+ (M,(f | B)))
let S be SigmaField of X; for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A, B being Element of S st ex E being Element of S st
( E = dom f & f is E -measurable ) & f is nonnegative & A misses B holds
integral+ (M,(f | (A \/ B))) = (integral+ (M,(f | A))) + (integral+ (M,(f | B)))
let M be sigma_Measure of S; for f being PartFunc of X,ExtREAL
for A, B being Element of S st ex E being Element of S st
( E = dom f & f is E -measurable ) & f is nonnegative & A misses B holds
integral+ (M,(f | (A \/ B))) = (integral+ (M,(f | A))) + (integral+ (M,(f | B)))
let f be PartFunc of X,ExtREAL; for A, B being Element of S st ex E being Element of S st
( E = dom f & f is E -measurable ) & f is nonnegative & A misses B holds
integral+ (M,(f | (A \/ B))) = (integral+ (M,(f | A))) + (integral+ (M,(f | B)))
let A, B be Element of S; ( ex E being Element of S st
( E = dom f & f is E -measurable ) & f is nonnegative & A misses B implies integral+ (M,(f | (A \/ B))) = (integral+ (M,(f | A))) + (integral+ (M,(f | B))) )
assume that
A1:
ex E being Element of S st
( E = dom f & f is E -measurable )
and
A2:
f is nonnegative
and
A3:
A misses B
; integral+ (M,(f | (A \/ B))) = (integral+ (M,(f | A))) + (integral+ (M,(f | B)))
consider F0 being Functional_Sequence of X,ExtREAL, K0 being ExtREAL_sequence such that
A4:
for n being Nat holds
( F0 . n is_simple_func_in S & dom (F0 . n) = dom f )
and
A5:
for n being Nat holds F0 . 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
(F0 . n) . x <= (F0 . m) . x
and
A7:
for x being Element of X st x in dom f holds
( F0 # x is convergent & lim (F0 # x) = f . x )
and
for n being Nat holds K0 . n = integral' (M,(F0 . n))
and
K0 is convergent
and
integral+ (M,f) = lim K0
by A1, A2, Def15;
deffunc H1( Nat) -> Element of bool [:X,ExtREAL:] = (F0 . $1) | B;
deffunc H2( Nat) -> Element of bool [:X,ExtREAL:] = (F0 . $1) | A;
consider FA being Functional_Sequence of X,ExtREAL such that
A8:
for n being Nat holds FA . n = H2(n)
from SEQFUNC:sch 1();
consider E being Element of S such that
A9:
E = dom f
and
A10:
f is E -measurable
by A1;
consider FB being Functional_Sequence of X,ExtREAL such that
A11:
for n being Nat holds FB . n = H1(n)
from SEQFUNC:sch 1();
set DB = E /\ B;
A12:
E /\ B = dom (f | B)
by A9, RELAT_1:61;
then A13:
(dom f) /\ (E /\ B) = E /\ B
by RELAT_1:60, XBOOLE_1:28;
then A14:
dom (f | (E /\ B)) = dom (f | B)
by A12, RELAT_1:61;
for x being object st x in dom (f | (E /\ B)) holds
(f | (E /\ B)) . x = (f | B) . x
then A16:
f | (E /\ B) = f | B
by A12, A13, FUNCT_1:2, RELAT_1:61;
set DA = E /\ A;
A17:
E /\ A = dom (f | A)
by A9, RELAT_1:61;
then A18:
(dom f) /\ (E /\ A) = E /\ A
by RELAT_1:60, XBOOLE_1:28;
then A19:
dom (f | (E /\ A)) = dom (f | A)
by A17, RELAT_1:61;
for x being object st x in dom (f | (E /\ A)) holds
(f | (E /\ A)) . x = (f | A) . x
then A21:
f | (E /\ A) = f | A
by A17, A18, FUNCT_1:2, RELAT_1:61;
A22:
for n being Nat holds
( FA . n is_simple_func_in S & FB . n is_simple_func_in S & dom (FA . n) = dom (f | A) & dom (FB . n) = dom (f | B) )
A26:
for x being Element of X st x in dom (f | A) holds
( FA # x is convergent & lim (FA # x) = (f | A) . x )
A31:
for x being Element of X st x in dom (f | B) holds
( FB # x is convergent & lim (FB # x) = (f | B) . x )
set C = E /\ (A \/ B);
A36:
E /\ (A \/ B) = (dom f) /\ (E /\ (A \/ B))
by A9, XBOOLE_1:17, XBOOLE_1:28;
A37:
dom (f | (A \/ B)) = E /\ (A \/ B)
by A9, RELAT_1:61;
then A38:
dom (f | (A \/ B)) = dom (f | (E /\ (A \/ B)))
by A36, RELAT_1:61;
for x being object st x in dom (f | (A \/ B)) holds
(f | (A \/ B)) . x = (f | (E /\ (A \/ B))) . x
then A40:
f | (A \/ B) = f | (E /\ (A \/ B))
by A38, FUNCT_1:2;
f is E /\ (A \/ B) -measurable
by A10, MESFUNC1:30, XBOOLE_1:17;
then A41:
f | (A \/ B) is E /\ (A \/ B) -measurable
by A36, A40, Th42;
f is E /\ B -measurable
by A10, MESFUNC1:30, XBOOLE_1:17;
then A42:
f | B is E /\ B -measurable
by A13, A16, Th42;
A43:
f | B is nonnegative
by A2, Th15;
f is E /\ A -measurable
by A10, MESFUNC1:30, XBOOLE_1:17;
then A44:
f | A is E /\ A -measurable
by A18, A21, Th42;
A45:
f | A is nonnegative
by A2, Th15;
deffunc H3( Nat) -> Element of bool [:X,ExtREAL:] = (F0 . $1) | (A \/ B);
consider FAB being Functional_Sequence of X,ExtREAL such that
A46:
for n being Nat holds FAB . n = H3(n)
from SEQFUNC:sch 1();
A47:
for n being Nat holds
( FA . n is nonnegative & FB . n is nonnegative )
A49:
for n, m being Nat st n <= m holds
for x being Element of X st x in dom (f | B) holds
(FB . n) . x <= (FB . m) . x
deffunc H4( Nat) -> Element of ExtREAL = integral' (M,(FA . $1));
consider KA being ExtREAL_sequence such that
A56:
for n being Element of NAT holds KA . n = H4(n)
from FUNCT_2:sch 4();
deffunc H5( Nat) -> Element of ExtREAL = integral' (M,(FB . $1));
consider KB being ExtREAL_sequence such that
A57:
for n being Element of NAT holds KB . n = H5(n)
from FUNCT_2:sch 4();
A58:
now for n being Nat holds KB . n = H5(n)end;
A59:
now for n being Nat holds KA . n = H4(n)end;
A60:
for n being set holds
( ( n in dom KA implies -infty < KA . n ) & ( n in dom KB implies -infty < KB . n ) )
then A63:
KB is ()
by Th10;
deffunc H6( Nat) -> Element of ExtREAL = integral' (M,(FAB . $1));
consider KAB being ExtREAL_sequence such that
A64:
for n being Element of NAT holds KAB . n = H6(n)
from FUNCT_2:sch 4();
A65:
now for n being Nat holds KAB . n = H6(n)end;
A66:
for n being Nat holds KAB . n = (KA . n) + (KB . n)
proof
let n be
Nat;
KAB . n = (KA . n) + (KB . n)
reconsider n =
n as
Element of
NAT by ORDINAL1:def 12;
A67:
FA . n = (F0 . n) | A
by A8;
A68:
FB . n = (F0 . n) | B
by A11;
A69:
KAB . n =
integral' (
M,
(FAB . n))
by A65
.=
integral' (
M,
((F0 . n) | (A \/ B)))
by A46
;
A70:
KA . n = integral' (
M,
(FA . n))
by A59;
F0 . n is_simple_func_in S
by A4;
then
integral' (
M,
((F0 . n) | (A \/ B)))
= (integral' (M,(FA . n))) + (integral' (M,(FB . n)))
by A3, A5, A67, A68, Th67;
hence
KAB . n = (KA . n) + (KB . n)
by A58, A69, A70;
verum
end;
A71:
for n, m being Nat st n <= m holds
for x being Element of X st x in dom (f | A) holds
(FA . n) . x <= (FA . m) . x
A78:
for n, m being Nat st n <= m holds
( KA . n <= KA . m & KB . n <= KB . m )
proof
let n,
m be
Nat;
( n <= m implies ( KA . n <= KA . m & KB . n <= KB . m ) )
A79:
FA . m is_simple_func_in S
by A22;
A80:
dom (FA . m) = dom (f | A)
by A22;
A81:
KA . m = integral' (
M,
(FA . m))
by A59;
A82:
dom (FA . n) = dom (f | A)
by A22;
assume A83:
n <= m
;
( KA . n <= KA . m & KB . n <= KB . m )
A84:
for
x being
object st
x in dom ((FA . m) - (FA . n)) holds
(FA . n) . x <= (FA . m) . x
A85:
FA . m is
nonnegative
by A47;
A86:
FA . n is
nonnegative
by A47;
A87:
FA . n is_simple_func_in S
by A22;
then A88:
dom ((FA . m) - (FA . n)) = (dom (FA . m)) /\ (dom (FA . n))
by A79, A86, A85, A84, Th69;
then A89:
(FA . m) | (dom ((FA . m) - (FA . n))) = FA . m
by A82, A80, GRFUNC_1:23;
A90:
(FA . n) | (dom ((FA . m) - (FA . n))) = FA . n
by A82, A80, A88, GRFUNC_1:23;
integral' (
M,
((FA . n) | (dom ((FA . m) - (FA . n)))))
<= integral' (
M,
((FA . m) | (dom ((FA . m) - (FA . n)))))
by A87, A79, A86, A85, A84, Th70;
hence
KA . n <= KA . m
by A59, A81, A89, A90;
KB . n <= KB . m
A91:
FB . m is_simple_func_in S
by A22;
A92:
FB . n is
nonnegative
by A47;
A93:
FB . m is
nonnegative
by A47;
A94:
KB . m = integral' (
M,
(FB . m))
by A58;
A95:
dom (FB . m) = dom (f | B)
by A22;
A96:
dom (FB . n) = dom (f | B)
by A22;
A97:
for
x being
object st
x in dom ((FB . m) - (FB . n)) holds
(FB . n) . x <= (FB . m) . x
A98:
FB . n is_simple_func_in S
by A22;
then A99:
dom ((FB . m) - (FB . n)) = (dom (FB . m)) /\ (dom (FB . n))
by A91, A92, A93, A97, Th69;
then A100:
(FB . m) | (dom ((FB . m) - (FB . n))) = FB . m
by A96, A95, GRFUNC_1:23;
A101:
(FB . n) | (dom ((FB . m) - (FB . n))) = FB . n
by A96, A95, A99, GRFUNC_1:23;
integral' (
M,
((FB . n) | (dom ((FB . m) - (FB . n)))))
<= integral' (
M,
((FB . m) | (dom ((FB . m) - (FB . n)))))
by A98, A91, A92, A93, A97, Th70;
hence
KB . n <= KB . m
by A58, A94, A100, A101;
verum
end;
then A102:
for n, m being Nat st n <= m holds
KA . n <= KA . m
;
then
KA is convergent
by Th54;
then A103:
integral+ (M,(f | A)) = lim KA
by A17, A44, A45, A22, A47, A71, A26, A59, Def15;
A104:
( ( for n being Nat holds
( FAB . n is_simple_func_in S & dom (FAB . n) = dom (f | (A \/ B)) ) ) & ( for n being Nat
for x being Element of X st x in dom (f | (A \/ B)) holds
(FAB . n) . x = (F0 . n) . x ) & ( for n being Nat holds FAB . n is nonnegative ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in dom (f | (A \/ B)) holds
(FAB . n) . x <= (FAB . m) . x ) & ( for x being Element of X st x in dom (f | (A \/ B)) holds
( FAB # x is convergent & lim (FAB # x) = (f | (A \/ B)) . x ) ) )
for n, m being Nat st n <= m holds
KAB . n <= KAB . m
proof
let n,
m be
Nat;
( n <= m implies KAB . n <= KAB . m )
assume A115:
n <= m
;
KAB . n <= KAB . m
reconsider n =
n,
m =
m as
Element of
NAT by ORDINAL1:def 12;
A116:
dom (FAB . m) = dom (f | (A \/ B))
by A104;
A117:
dom (FAB . n) = dom (f | (A \/ B))
by A104;
A118:
for
x being
object st
x in dom ((FAB . m) - (FAB . n)) holds
(FAB . n) . x <= (FAB . m) . x
A119:
KAB . m = integral' (
M,
(FAB . m))
by A65;
A120:
FAB . m is_simple_func_in S
by A104;
A121:
FAB . m is
nonnegative
by A104;
A122:
FAB . n is
nonnegative
by A104;
A123:
FAB . n is_simple_func_in S
by A104;
then A124:
dom ((FAB . m) - (FAB . n)) = (dom (FAB . m)) /\ (dom (FAB . n))
by A120, A122, A121, A118, Th69;
then A125:
(FAB . m) | (dom ((FAB . m) - (FAB . n))) = FAB . m
by A117, A116, GRFUNC_1:23;
A126:
(FAB . n) | (dom ((FAB . m) - (FAB . n))) = FAB . n
by A117, A116, A124, GRFUNC_1:23;
integral' (
M,
((FAB . n) | (dom ((FAB . m) - (FAB . n)))))
<= integral' (
M,
((FAB . m) | (dom ((FAB . m) - (FAB . n)))))
by A123, A120, A122, A121, A118, Th70;
hence
KAB . n <= KAB . m
by A65, A119, A125, A126;
verum
end;
then A127:
KAB is convergent
by Th54;
A128:
for n, m being Nat st n <= m holds
KB . n <= KB . m
by A78;
then
KB is convergent
by Th54;
then A129:
integral+ (M,(f | B)) = lim KB
by A12, A42, A43, A22, A47, A49, A31, A58, Def15;
f | (A \/ B) is nonnegative
by A2, Th15;
then A130:
integral+ (M,(f | (A \/ B))) = lim KAB
by A37, A41, A65, A104, A127, Def15;
KA is ()
by A60, Th10;
hence
integral+ (M,(f | (A \/ B))) = (integral+ (M,(f | A))) + (integral+ (M,(f | B)))
by A130, A102, A128, A103, A129, A66, A63, Th61; verum