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