theorem Th10: :: FINSEQ_7:10

for D being non empty set
for f being FinSequence of D
for p being Element of D
for i, k being Nat st 1 <= k & k <= len f & k <> i holds
(Replace (f,i,p)) /. k = f /. k