for i being Nat
for k being Element of NAT
for q being FinSubsequence st dom q c= Seg k holds
dom (Shift (q,i)) c= Seg (i + k)