set ap = p * a;
A4: Support p is finite by POLYNOM1:def 10;

now

let u be set ; :: thesis: ( u in Support (p * a) implies u in Support p )
assume A5: u in Support (p * a) ; :: thesis: u in Support p
then A6: (p * a) . u <> 0. L by POLYNOM1:def 9;
reconsider u' = u as Element of Bags X by A5;
(p . u') * a <> 0. L by A6, Def11;
then p . u' <> 0. L by BINOM:1;
hence u in Support p by POLYNOM1:def 9; :: thesis: verum

end;

then Support (p * a) c= Support p by TARSKI:def 3;
then Support (p * a) is finite by A4;
hence p * a is finite-Support by POLYNOM1:def 10; :: thesis: verum