for i being Nat
for x, y being set
for f being NAT -defined non empty finite Function holds Shift ((f +~ (x,y)),i) = (Shift (f,i)) +~ (x,y)