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