theorem :: POLYNOM4:21

for L being non empty right_complementable Abelian add-associative right_zeroed 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))