set ap = a * p;

now :: thesis: for u being object st u in Support (a * p) holds
u in Support p

let u be object ; :: thesis: ( u in Support (a * p) implies u in Support p )
assume A1: u in Support (a * p) ; :: thesis: u in Support p
then reconsider u9 = u as Element of Bags X ;
(a * p) . u <> 0. L by A1, POLYNOM1:def 4;
then a * (p . u9) <> 0. L by Def9;
then p . u9 <> 0. L by BINOM:2;
hence u in Support p by POLYNOM1:def 4; :: thesis: verum

end;

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