let X1, X2 be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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)); :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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; :: thesis: (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; :: thesis: 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; :: thesis: 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; :: thesis: (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; :: thesis: 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; :: thesis: verum