for R being real Polynomial of F_Complex
for r being real Element of F_Complex holds eval (R,r) is real