theorem Th20: :: MEASUR13:20

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