theorem :: VALUED_1:46

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