theorem Th3: :: HILB10_2:3

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