set ap = a * p;

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

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

u in Support p

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

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