theorem Th16: :: POLYNOM9:16

for X being set
for x being object
for b being bag of X holds support (b +* (x,0)) = (support b) \ {x}