for L being non empty right_complementable Abelian add-associative right_zeroed left-distributive unital doubleLoopStr
for p, q being Polynomial of L
for x being Element of L holds eval ((p + q),x) = (eval (p,x)) + (eval (q,x))