theorem Th11: :: HILB10_2:11

for n being Nat
for b being bag of n holds support b = support (b bag_extend 0)