for L being non degenerated comRing
for x being Element of L
for n being Element of NAT
for p being Polynomial of L st n < len p holds
eval ((poly_shift (p,n)),x) = (x * (eval ((poly_shift (p,(n + 1))),x))) + (p . n)