for L being non empty ZeroStr
for p being Polynomial of L st len p = 0 holds
Leading-Monomial p = 0_. L