set ap = p * a;
now :: thesis: for u being object st u in Support (p * a) holds
u in Support p
let u be object ; :: 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 4;
then (p . u9) * a <> 0. L by Def10;
then p . u9 <> 0. L by BINOM:1;
hence u in Support p by POLYNOM1:def 4; :: thesis: verum
end;
then ( Support p is finite & Support (p * a) c= Support p ) by POLYNOM1:def 5, TARSKI:def 3;
hence p * a is finite-Support by POLYNOM1:def 5; :: thesis: verum