theorem Th59: :: FINSEQ_5:59

for f being FinSequence
for i, j being Nat st i in dom f & i + j = (len f) + 1 holds
j in dom (Rev f)