let X1, X2 be non empty set ; :: thesis: for S1 being SigmaField of X1
for S2 being SigmaField of X2
for E being Element of sigma (measurable_rectangles (S1,S2)) holds
( ( for p being set holds X-section (E,p) in S2 ) & ( for p being set holds Y-section (E,p) in S1 ) )
let S1 be SigmaField of X1; :: thesis: for S2 being SigmaField of X2
for E being Element of sigma (measurable_rectangles (S1,S2)) holds
( ( for p being set holds X-section (E,p) in S2 ) & ( for p being set holds Y-section (E,p) in S1 ) )
let S2 be SigmaField of X2; :: thesis: for E being Element of sigma (measurable_rectangles (S1,S2)) holds
( ( for p being set holds X-section (E,p) in S2 ) & ( for p being set holds Y-section (E,p) in S1 ) )
let E be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: ( ( for p being set holds X-section (E,p) in S2 ) & ( for p being set holds Y-section (E,p) in S1 ) )
set K = { C where C is Subset of [:X1,X2:] : for x being set holds X-section (C,x) in S2 } ;
reconsider K = { C where C is Subset of [:X1,X2:] : for x being set holds X-section (C,x) in S2 } as SigmaField of [:X1,X2:] by Th42;
A1: ( measurable_rectangles (S1,S2) c= Field_generated_by (measurable_rectangles (S1,S2)) & Field_generated_by (measurable_rectangles (S1,S2)) c= K ) by Th42, SRINGS_3:21;
then measurable_rectangles (S1,S2) c= K ;
then sigma (measurable_rectangles (S1,S2)) c= K by PROB_1:def 9;
then E in K ;
then ex C being Subset of [:X1,X2:] st
( E = C & ( for x being set holds X-section (C,x) in S2 ) ) ;
hence for x being set holds X-section (E,x) in S2 ; :: thesis: for p being set holds Y-section (E,p) in S1
set K2 = { C where C is Subset of [:X1,X2:] : for x being set holds Y-section (C,x) in S1 } ;
reconsider K2 = { C where C is Subset of [:X1,X2:] : for x being set holds Y-section (C,x) in S1 } as SigmaField of [:X1,X2:] by Th43;
Field_generated_by (measurable_rectangles (S1,S2)) c= K2 by Th43;
then measurable_rectangles (S1,S2) c= K2 by A1;
then sigma (measurable_rectangles (S1,S2)) c= K2 by PROB_1:def 9;
then E in K2 ;
then ex C being Subset of [:X1,X2:] st
( E = C & ( for x being set holds Y-section (C,x) in S1 ) ) ;
hence for x being set holds Y-section (E,x) in S1 ; :: thesis: verum