for L being non empty ZeroStr
for p being Polynomial of L st 0 <= deg p holds
p is non-zero