theorem Th7: :: MEASUR13:7

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