set ap = p * a;

hence p * a is finite-Support by POLYNOM1:def 5; :: thesis: verum

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

u in Support p

then
( Support p is finite & Support (p * a) c= Support p )
by POLYNOM1:def 5, TARSKI:def 3;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;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

hence p * a is finite-Support by POLYNOM1:def 5; :: thesis: verum