theorem :: HURWITZ:21

for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p1, p2 being Polynomial of L st deg p1 <> deg p2 holds
deg (p1 + p2) = max ((deg p1),(deg p2))