theorem :: MSSCYC_1:8
for m, n being Nat
for f being FinSequence holds len ((m,n) -cut f) <= len f