consider b being Element of Support p;
set ap = a * p;
p <> 0_ (n,L) by POLYNOM7:def 2;
then A2: Support p <> {} by POLYNOM7:1;
then b in Support p ;
then reconsider b = b as Element of Bags n ;
p . b <> 0. L by A2, POLYNOM1:def 9;
then a * (p . b) <> 0. L by VECTSP_2:def 5;
then (a * p) . b <> 0. L by POLYNOM7:def 10;
then b in Support (a * p) by POLYNOM1:def 9;
then a * p <> 0_ (n,L) by POLYNOM7:1;
hence a * p is non-zero by POLYNOM7:def 2; :: thesis: verum