theorem Th22: :: LIOUVIL2:21

for f being REAL -valued Polynomial of F_Complex holds f is Polynomial of F_Real