let f be REAL -valued Polynomial of F_Complex; :: thesis: f is Polynomial of F_Real
rng f c= REAL ;
then reconsider f1 = f as sequence of F_Real by FUNCT_2:6;
f1 is finite-Support by Lm1, ALGSEQ_1:def 1;
hence f is Polynomial of F_Real ; :: thesis: verum