theorem Th9: :: MEASUR14:9

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