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 holds
( M1 . (Measurable-Y-section (E,y)) = Integral (M1,(ProjMap2 ((chi (E,[:X1,X2:])),y))) & M2 . (Measurable-X-section (E,x)) = Integral (M2,(ProjMap1 ((chi (E,[: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 holds
( M1 . (Measurable-Y-section (E,y)) = Integral (M1,(ProjMap2 ((chi (E,[:X1,X2:])),y))) & M2 . (Measurable-X-section (E,x)) = Integral (M2,(ProjMap1 ((chi (E,[: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 holds
( M1 . (Measurable-Y-section (E,y)) = Integral (M1,(ProjMap2 ((chi (E,[:X1,X2:])),y))) & M2 . (Measurable-X-section (E,x)) = Integral (M2,(ProjMap1 ((chi (E,[: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 holds
( M1 . (Measurable-Y-section (E,y)) = Integral (M1,(ProjMap2 ((chi (E,[:X1,X2:])),y))) & M2 . (Measurable-X-section (E,x)) = Integral (M2,(ProjMap1 ((chi (E,[: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 holds
( M1 . (Measurable-Y-section (E,y)) = Integral (M1,(ProjMap2 ((chi (E,[:X1,X2:])),y))) & M2 . (Measurable-X-section (E,x)) = Integral (M2,(ProjMap1 ((chi (E,[: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 holds
( M1 . (Measurable-Y-section (E,y)) = Integral (M1,(ProjMap2 ((chi (E,[:X1,X2:])),y))) & M2 . (Measurable-X-section (E,x)) = Integral (M2,(ProjMap1 ((chi (E,[:X1,X2:])),x))) )
let x be Element of X1; :: thesis: for y being Element of X2 holds
( M1 . (Measurable-Y-section (E,y)) = Integral (M1,(ProjMap2 ((chi (E,[:X1,X2:])),y))) & M2 . (Measurable-X-section (E,x)) = Integral (M2,(ProjMap1 ((chi (E,[:X1,X2:])),x))) )
let y be Element of X2; :: thesis: ( M1 . (Measurable-Y-section (E,y)) = Integral (M1,(ProjMap2 ((chi (E,[:X1,X2:])),y))) & M2 . (Measurable-X-section (E,x)) = Integral (M2,(ProjMap1 ((chi (E,[:X1,X2:])),x))) )
A1: ( X1 in S1 & X2 in S2 ) by MEASURE1:7;
( E /\ [:X1,X2:] = E & (Measurable-Y-section (E,y)) /\ X1 = Measurable-Y-section (E,y) & (Measurable-X-section (E,x)) /\ X2 = Measurable-X-section (E,x) ) by XBOOLE_1:28;
hence ( M1 . (Measurable-Y-section (E,y)) = Integral (M1,(ProjMap2 ((chi (E,[:X1,X2:])),y))) & M2 . (Measurable-X-section (E,x)) = Integral (M2,(ProjMap1 ((chi (E,[:X1,X2:])),x))) ) by Th67, A1; :: thesis: verum