for L being non empty ZeroStr
for p being Polynomial of L st p <> 0_. L holds
(len p) -' 1 = (len p) - 1