Support p is finite by POLYNOM1:def 4;
then Support (p | Y) is finite by Lm2, FINSET_1:1;
hence p | Y is finite-Support by POLYNOM1:def 4; :: thesis: verum