let X1, X2 be non empty set ; :: thesis: for S1 being SigmaField of X1
for S2 being SigmaField of X2
for F1 being Set_Sequence of S1
for F2 being Set_Sequence of S2
for n being Nat holds [:(F1 . n),(F2 . n):] is Element of sigma (measurable_rectangles (S1,S2))
let S1 be SigmaField of X1; :: thesis: for S2 being SigmaField of X2
for F1 being Set_Sequence of S1
for F2 being Set_Sequence of S2
for n being Nat holds [:(F1 . n),(F2 . n):] is Element of sigma (measurable_rectangles (S1,S2))
let S2 be SigmaField of X2; :: thesis: for F1 being Set_Sequence of S1
for F2 being Set_Sequence of S2
for n being Nat holds [:(F1 . n),(F2 . n):] is Element of sigma (measurable_rectangles (S1,S2))
let F1 be Set_Sequence of S1; :: thesis: for F2 being Set_Sequence of S2
for n being Nat holds [:(F1 . n),(F2 . n):] is Element of sigma (measurable_rectangles (S1,S2))
let F2 be Set_Sequence of S2; :: thesis: for n being Nat holds [:(F1 . n),(F2 . n):] is Element of sigma (measurable_rectangles (S1,S2))
let n be Nat; :: thesis: [:(F1 . n),(F2 . n):] is Element of sigma (measurable_rectangles (S1,S2))
set S = measurable_rectangles (S1,S2);
( F1 . n in S1 & F2 . n in S2 ) by MEASURE8:def 2;
then [:(F1 . n),(F2 . n):] in { [:A,B:] where A is Element of S1, B is Element of S2 : verum } ;
then A1: [:(F1 . n),(F2 . n):] in measurable_rectangles (S1,S2) by MEASUR10:def 5;
A2: measurable_rectangles (S1,S2) c= DisUnion (measurable_rectangles (S1,S2)) by SRINGS_3:12;
DisUnion (measurable_rectangles (S1,S2)) c= sigma (DisUnion (measurable_rectangles (S1,S2))) by PROB_1:def 9;
then [:(F1 . n),(F2 . n):] is Element of sigma (DisUnion (measurable_rectangles (S1,S2))) by A1, A2;
hence [:(F1 . n),(F2 . n):] is Element of sigma (measurable_rectangles (S1,S2)) by Th1; :: thesis: verum