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