theorem :: FINSEQ_5:66

for i, j being Nat
for D being non empty set
for f being FinSequence of D st i in dom f & i + j = (len f) + 1 holds
f /. i = (Rev f) /. j