theorem Th4: :: MEASUR13:4

for m, n being non zero Nat
for X being non-empty b₁ -element FinSequence st n <= m holds
(ProdFinSeq X) . n = (ProdFinSeq (SubFin (X,n))) . n