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