let p, q be Polynomial of F_Real; :: thesis: poly_diff (p - q) = (poly_diff p) - (poly_diff q)
thus poly_diff (p - q) = (poly_diff p) + (poly_diff (- q)) by Th47
.= (poly_diff p) - (poly_diff q) by Th48 ; :: thesis: verum