for L being non empty right_complementable well-unital distributive add-associative right_zeroed associative domRing-like doubleLoopStr
for p1, p2 being Polynomial of L st p1 <> 0_. L & p2 <> 0_. L holds
deg (p1 *' p2) = (deg p1) + (deg p2)