theorem Th33: :: UPROOTS:36

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 1 < len p & 1 < len q holds
len p < len (p *' q)