theorem Th4: :: HILB10_2:4

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