let X1, X2 be 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))) )
let S1 be 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))) )
let S2 be 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))) )
let M1 be 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))) )
let M2 be 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))) )
let E be 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))) )
let x be 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))) )
let y be 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))) )
let U be 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))) )
let V be Element of S2; ( 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))) )
for x being Element of X1 holds (ProjMap2 ((chi ((E /\ [:U,X2:]),[:X1,X2:])),y)) . x = (chi (((Measurable-Y-section (E,y)) /\ U),X1)) . x
proof
let x be
Element of
X1;
(ProjMap2 ((chi ((E /\ [:U,X2:]),[:X1,X2:])),y)) . x = (chi (((Measurable-Y-section (E,y)) /\ U),X1)) . x
A1:
X2 = [#] X2
by SUBSET_1:def 3;
(ProjMap2 ((chi ((E /\ [:U,X2:]),[:X1,X2:])),y)) . x =
(chi ((E /\ [:U,X2:]),[:X1,X2:])) . (
x,
y)
by MESFUNC9:def 7
.=
(chi ((Y-section ((E /\ [:U,X2:]),y)),X1)) . x
by Th28
.=
(chi (((Y-section (E,y)) /\ (Y-section ([:U,([#] X2):],y))),X1)) . x
by A1, Th21
;
hence
(ProjMap2 ((chi ((E /\ [:U,X2:]),[:X1,X2:])),y)) . x = (chi (((Measurable-Y-section (E,y)) /\ U),X1)) . x
by A1, Th16;
verum
end;
then
ProjMap2 ((chi ((E /\ [:U,X2:]),[:X1,X2:])),y) = chi (((Measurable-Y-section (E,y)) /\ U),X1)
by FUNCT_2:def 8;
hence
M1 . ((Measurable-Y-section (E,y)) /\ U) = Integral (M1,(ProjMap2 ((chi ((E /\ [:U,X2:]),[:X1,X2:])),y)))
by MESFUNC9:14; M2 . ((Measurable-X-section (E,x)) /\ V) = Integral (M2,(ProjMap1 ((chi ((E /\ [:X1,V:]),[:X1,X2:])),x)))
for y being Element of X2 holds (ProjMap1 ((chi ((E /\ [:X1,V:]),[:X1,X2:])),x)) . y = (chi (((Measurable-X-section (E,x)) /\ V),X2)) . y
proof
let y be
Element of
X2;
(ProjMap1 ((chi ((E /\ [:X1,V:]),[:X1,X2:])),x)) . y = (chi (((Measurable-X-section (E,x)) /\ V),X2)) . y
A3:
X1 = [#] X1
by SUBSET_1:def 3;
(ProjMap1 ((chi ((E /\ [:X1,V:]),[:X1,X2:])),x)) . y =
(chi ((E /\ [:X1,V:]),[:X1,X2:])) . (
x,
y)
by MESFUNC9:def 6
.=
(chi ((X-section ((E /\ [:X1,V:]),x)),X2)) . y
by Th28
.=
(chi (((X-section (E,x)) /\ (X-section ([:([#] X1),V:],x))),X2)) . y
by A3, Th21
;
hence
(ProjMap1 ((chi ((E /\ [:X1,V:]),[:X1,X2:])),x)) . y = (chi (((Measurable-X-section (E,x)) /\ V),X2)) . y
by A3, Th16;
verum
end;
then
ProjMap1 ((chi ((E /\ [:X1,V:]),[:X1,X2:])),x) = chi (((Measurable-X-section (E,x)) /\ V),X2)
by FUNCT_2:def 8;
hence
M2 . ((Measurable-X-section (E,x)) /\ V) = Integral (M2,(ProjMap1 ((chi ((E /\ [:X1,V:]),[:X1,X2:])),x)))
by MESFUNC9:14; verum