theorem :: POLYVIE1:5

for L being non trivial ZeroStr
for p being Polynomial of L st len p = 1 holds
ex a being non zero Element of L st p = <%a%>