theorem
for
X1,
X2 being non
empty set for
S1 being
SigmaField of
X1 for
S2 being
SigmaField of
X2 for
M1 being
sigma_Measure of
S1 for
M2 being
sigma_Measure of
S2 for
E,
E1,
E2 being
Element of
sigma (measurable_rectangles (S1,S2)) for
f being
PartFunc of
[:X1,X2:],
ExtREAL st
E = dom f & (
f is
nonnegative or
f is
nonpositive ) &
f is
E -measurable &
E1 misses E2 holds
(
Integral1 (
M1,
(f | (E1 \/ E2)))
= (Integral1 (M1,(f | E1))) + (Integral1 (M1,(f | E2))) &
Integral2 (
M2,
(f | (E1 \/ E2)))
= (Integral2 (M2,(f | E1))) + (Integral2 (M2,(f | E2))) )
by Lm11, Lm12;