theorem Th19: :: MEASUR13:19

for m, n being non zero Nat
for X being non-empty b₁ -element FinSequence
for S being sigmaFieldFamily of X st n <= m holds
(ProdSigmaFldFinSeq S) . n is SigmaField of ((ProdFinSeq X) . n)