let m, n be non zero Nat; :: thesis: for X being non-empty m -element FinSequence
for S being sigmaFieldFamily of X st n < m holds
Prod_Field (SubFin (S,(n + 1))) = sigma (measurable_rectangles ((Prod_Field (SubFin (S,n))),(ElmFin (S,(n + 1)))))
let X be non-empty m -element FinSequence; :: thesis: for S being sigmaFieldFamily of X st n < m holds
Prod_Field (SubFin (S,(n + 1))) = sigma (measurable_rectangles ((Prod_Field (SubFin (S,n))),(ElmFin (S,(n + 1)))))
let S be sigmaFieldFamily of X; :: thesis: ( n < m implies Prod_Field (SubFin (S,(n + 1))) = sigma (measurable_rectangles ((Prod_Field (SubFin (S,n))),(ElmFin (S,(n + 1))))) )
assume A1: n < m ; :: thesis: Prod_Field (SubFin (S,(n + 1))) = sigma (measurable_rectangles ((Prod_Field (SubFin (S,n))),(ElmFin (S,(n + 1)))))
then A2: n + 1 <= m by NAT_1:13;
then A3: ElmFin ((SubFin (X,(n + 1))),(n + 1)) = ElmFin (X,(n + 1)) by Th8;
A4: ElmFin ((SubFin (S,(n + 1))),(n + 1)) = ElmFin (S,(n + 1)) by A2, Th12;
A5: n < n + 1 by NAT_1:13;
then A6: CarProduct (SubFin ((SubFin (X,(n + 1))),n)) = CarProduct (SubFin (X,n)) by A2, Th7;
consider Sn being SigmaField of (CarProduct (SubFin ((SubFin (X,(n + 1))),n))) such that
A7: ( Sn = (ProdSigmaFldFinSeq (SubFin (S,(n + 1)))) . n & (ProdSigmaFldFinSeq (SubFin (S,(n + 1)))) . (n + 1) = sigma (measurable_rectangles (Sn,(ElmFin ((SubFin (S,(n + 1))),(n + 1))))) ) by A5, Def11;
Sn = (ProdSigmaFldFinSeq S) . n by A5, A7, A2, Th20;
hence Prod_Field (SubFin (S,(n + 1))) = sigma (measurable_rectangles ((Prod_Field (SubFin (S,n))),(ElmFin (S,(n + 1))))) by A7, A4, A3, A6, A1, Th20; :: thesis: verum