:: deftheorem Def11 defines ProdSigmaFldFinSeq MEASUR13:def 11 :
for m being non zero Nat
for X being non-empty b₁ -element FinSequence
for S being sigmaFieldFamily of X
for b₄ being sigmaFieldFamily of ProdFinSeq X holds
( b₄ = ProdSigmaFldFinSeq S iff ( b₄ . 1 = S . 1 & ( for i being non zero Nat st i < m holds
ex Si being SigmaField of (CarProduct (SubFin (X,i))) st
( Si = b₄ . i & b₄ . (i + 1) = sigma (measurable_rectangles (Si,(ElmFin (S,(i + 1))))) ) ) ) );