let i be Nat; :: thesis: for f being FinSequence st i in dom f holds
(Rev f) . i = f . (((len f) - i) + 1)
let f be FinSequence; :: thesis: ( i in dom f implies (Rev f) . i = f . (((len f) - i) + 1) )
dom f = dom (Rev f) by Th57;
hence ( i in dom f implies (Rev f) . i = f . (((len f) - i) + 1) ) by Def3; :: thesis: verum