for i being Nat
for k being Element of NAT
for p being FinSequence st k in dom p holds
(Sgm (dom (Shift (p,i)))) . k = i + k