for L being non empty ZeroStr
for n being Element of NAT
for p being Polynomial of L st n >= len p holds
poly_shift (p,n) = 0_. L