theorem Th9: :: POLYNOM8:9

for L being non empty right_complementable well-unital distributive add-associative right_zeroed associative commutative domRing-like doubleLoopStr
for p, q being Polynomial of L st len p > 0 & len q > 0 holds
len (p *' q) <= (len p) + (len q)