theorem Th15: :: BASEL_2:15

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