:: deftheorem defines non-zero POLYNOM7:def 1 :
for X being set
for R being non empty ZeroStr
for p being Series of X,R holds
( p is non-zero iff p <> 0_ (X,R) );