theorem :: POLYRED:20

for n being Ordinal
for L being non trivial domRing-like doubleLoopStr
for p being Polynomial of n,L
for a being non zero Element of L holds Support p c= Support (a * p)