theorem Th8: :: MEASUR13:8

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