theorem :: MEASUR13:10

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