theorem Th9: :: POLYNOM2:17

for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for n being Ordinal
for p being Polynomial of n,L st Support p = {} holds
p = 0_ (n,L)