for i being Nat
for q being FinSubsequence holds Seq q = Seq (Shift (q,i))