for i being Element of NAT
for y being set
for f being FinSubsequence st f = {[1,y]} holds
Shift (f,i) = {[(1 + i),y]}