theorem Th6: :: HILBASIS:6

for n being Nat holds EmptyBag (n + 1) = (EmptyBag n) bag_extend 0