:: deftheorem Def5 defines poly_shift UPROOTS:def 6 :
for L being non empty ZeroStr
for p being Polynomial of L
for n being Nat
for b₄ being Polynomial of L holds
( b₄ = poly_shift (p,n) iff for i being Nat holds b₄ . i = p . (n + i) );