for n being Nat
for L being non empty ZeroStr
for p being Polynomial of L st n > (len p) -' 1 holds
p || n = p