:: deftheorem Def4 defines non-zero UPROOTS:def 5 :
for L being non empty ZeroStr
for p being Polynomial of L holds
( p is non-zero iff p <> 0_. L );