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