theorem :: VALUED_1:59

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