for F being NAT -defined total Function
for p being NAT -defined Function
for n being Element of NAT st Shift (p,n) c= F holds
for i being Element of NAT st i in dom p holds
F . (n + i) = p . i