theorem Th74:
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
f,
g being
PartFunc of
[:X1,X2:],
ExtREAL for
E1,
E2 being
Element of
sigma (measurable_rectangles (S1,S2)) st
E1 = dom f &
f is
nonnegative &
f is
E1 -measurable &
E2 = dom g &
g is
nonnegative &
g is
E2 -measurable holds
(
Integral1 (
M1,
(f + g))
= (Integral1 (M1,(f | (dom (f + g))))) + (Integral1 (M1,(g | (dom (f + g))))) &
Integral2 (
M2,
(f + g))
= (Integral2 (M2,(f | (dom (f + g))))) + (Integral2 (M2,(g | (dom (f + g))))) )