theorem Th7: :: POLYNOM9:7

for n being Nat
for X being set
for b being bag of X holds support (n (#) b) c= support b