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