theorem Th5: :: MEASUR13:5

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