set ap = a * p;
p <> 0_ n,L by POLYNOM7:def 2;
then A1: Support p <> {} by POLYNOM7:1;
consider b being Element of Support p;
b in Support p by A1;
then reconsider b = b as Element of Bags n ;
A2: p . b <> 0. L by A1, POLYNOM1:def 9;
a <> 0. L by STRUCT_0:def 15;
then a * (p . b) <> 0. L by A2, 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