theorem Th4: :: JORDAN9:4

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