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