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

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