:: deftheorem Def1 defines zero RATFUNC1:def 1 :
for L being non empty ZeroStr
for p being Polynomial of L holds
( p is zero iff p = 0_. L );