theorem :: POLYRED:14

for n being Ordinal
for L being non empty ZeroStr
for p being Polynomial of n,L
for b being bag of n holds Support (b *' p) c= { (b + b9) where b9 is Element of Bags n : b9 in Support p } by Lm10;