let p, q be Polynomial of F_Real; :: thesis: Eval (p - q) = (Eval p) - (Eval q)
thus Eval (p - q) = (Eval p) + (Eval (- q)) by Th55
.= (Eval p) - (Eval q) by Th56 ; :: thesis: verum