theorem :: FINSEQ_5:66

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