set ap = a * p;
A1: Support p is finite by POLYNOM1:def 5;
Support (a * p) c= Support p

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in Support (a * p) or u in Support p )
assume A2: ( u in Support (a * p) & not u in Support p ) ; :: thesis: contradiction
A3: ( dom (a * p) = Bags X & Bags X = dom p ) by FUNCT_2:def 1;
reconsider u = u as bag of X by A2;
A4: ( a * (p . u) = (a * p) . u & (a * p) . u <> 0. L & u in dom p ) by A3, A2, POLYNOM1:def 3, POLYNOM7:def 9;
p . u = 0. L by A2, POLYNOM1:def 3, A3;
hence contradiction by A4; :: thesis: verum

end;

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