theorem Th10: :: MEASUR14:10

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