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