theorem Th40: :: NIVEN:42

for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p, q being Polynomial of L st deg p > deg q holds
deg (p + q) = deg p