set ap = p * a;

now

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

end;

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