for k being Nat
for D being set
for f being FinSequence of D st k <= len f holds
(1,k) -cut f = f | k