for k, n being Nat
for b being ManySortedSet of n st k <= n holds
(0,k) -cut b = b | k