for i being Nat
for p being FinSequence holds Seq (Shift (p,i)) = p