theorem :: POLYNOM9:9

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