theorem Th82:
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 being
Element of
sigma (measurable_rectangles (S1,S2)) st
M1 is
sigma_finite &
M2 is
sigma_finite holds
(
Integral (
(Prod_Measure (M1,M2)),
(chi (E,[:X1,X2:])))
= Integral (
M2,
(Integral1 (M1,(chi (E,[:X1,X2:]))))) &
Integral (
(Prod_Measure (M1,M2)),
((chi (E,[:X1,X2:])) | E))
= Integral (
M2,
(Integral1 (M1,((chi (E,[:X1,X2:])) | E)))) &
Integral (
(Prod_Measure (M1,M2)),
(chi (E,[:X1,X2:])))
= Integral (
M1,
(Integral2 (M2,(chi (E,[:X1,X2:]))))) &
Integral (
(Prod_Measure (M1,M2)),
((chi (E,[:X1,X2:])) | E))
= Integral (
M1,
(Integral2 (M2,((chi (E,[:X1,X2:])) | E)))) )