theorem Th58: :: FINSEQ_5:58

for i being Nat
for f being FinSequence st i in dom f holds
(Rev f) . i = f . (((len f) - i) + 1)