for f being Function
for i, n being Nat st i in dom (Shift (f,n)) holds
ex j being Nat st
( j in dom f & i = j + n )