theorem Th8: :: MEASUR14:8

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
( SubFin ((SubFin (X,n1)),k) = SubFin ((SubFin (X,n2)),k) & ElmFin ((SubFin (X,n1)),k) = ElmFin ((SubFin (X,n2)),k) )