for p being constant Polynomial of F_Real holds poly_diff p = 0_. F_Real