theorem Th65:
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)) for
A being
Element of
S1 for
B being
Element of
S2 for
x being
Element of
X1 for
y being
Element of
X2 st
E = [:A,B:] holds
(
Integral (
M2,
(ProjMap1 ((chi (E,[:X1,X2:])),x)))
= (M2 . (Measurable-X-section (E,x))) * ((chi (A,X1)) . x) &
Integral (
M1,
(ProjMap2 ((chi (E,[:X1,X2:])),y)))
= (M1 . (Measurable-Y-section (E,y))) * ((chi (B,X2)) . y) )