for n being Nat
for b being bag of n + 1 holds b = ((0,n) -cut b) bag_extend (b . n)