let f be INT -valued Polynomial of F_Rat; :: thesis: f is Polynomial of INT.Ring
rng f c= INT ;
then reconsider f1 = f as sequence of INT.Ring by FUNCT_2:6;
0. F_Rat = 0 by GAUSSINT:def 14;
then f1 is finite-Support by ALGSEQ_1:def 1;
hence f is Polynomial of INT.Ring ; :: thesis: verum