let n be non zero Nat; :: thesis: for X being non-empty n + 1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S holds Prod_Field S = sigma (measurable_rectangles ((Prod_Field (SubFin (S,n))),(ElmFin (S,(n + 1)))))
let X be non-empty n + 1 -element FinSequence; :: thesis: for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S holds Prod_Field S = sigma (measurable_rectangles ((Prod_Field (SubFin (S,n))),(ElmFin (S,(n + 1)))))
let S be sigmaFieldFamily of X; :: thesis: for M being sigmaMeasureFamily of S holds Prod_Field S = sigma (measurable_rectangles ((Prod_Field (SubFin (S,n))),(ElmFin (S,(n + 1)))))
let M be sigmaMeasureFamily of S; :: thesis: Prod_Field S = sigma (measurable_rectangles ((Prod_Field (SubFin (S,n))),(ElmFin (S,(n + 1)))))
A1: n < n + 1 by NAT_1:13;
A2: len X = n + 1 by CARD_1:def 7;
SubFin (X,(n + 1)) = X | (n + 1) by Def5;
then A3: X = SubFin (X,(n + 1)) by A2, FINSEQ_1:58;
A4: len S = n + 1 by CARD_1:def 7;
SubFin (S,(n + 1)) = S | (n + 1) by Def6;
then S = SubFin (S,(n + 1)) by A4, FINSEQ_1:58;
hence Prod_Field S = sigma (measurable_rectangles ((Prod_Field (SubFin (S,n))),(ElmFin (S,(n + 1))))) by A3, A1, Th21; :: thesis: verum