set ap = a * p;
A1: Support p is finite by POLYNOM1:def 10;

now

now

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

end;

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

end;

hence a * p is finite-Support ; :: thesis: verum