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

then Support (p | Y) is finite by Lm2, FINSET_1:1;

hence p | Y is finite-Support by POLYNOM1:def 5; :: thesis: verum