theorem Th114: :: FINSEQ_6:115

for D being non empty set
for i being Nat
for f being FinSequence of D st 1 <= i & i <= len f holds
(Rev f) . i = f . (((len f) - i) + 1)