theorem Th27: :: FINSEQ_5:27

for i, n being Nat
for D being set
for f being FinSequence of D st i in dom (f /^ n) holds
(f /^ n) /. i = f /. (n + i)