theorem :: POLYDIFF:57

for p, q being Polynomial of F_Real holds Eval (p - q) = (Eval p) - (Eval q)