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