theorem Th3: :: JORDAN9:3

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