A1: dom (Rev f) = dom f by FINSEQ_5:57;
for i being object st i in dom f holds
(Rev f) . i = f . i

proof

let i be object ; :: thesis: ( i in dom f implies (Rev f) . i = f . i )
assume B1: i in dom f ; :: thesis: (Rev f) . i = f . i
B2: i in dom (Rev f) by B1, FINSEQ_5:57;
reconsider i = i as Nat by B1;
set n = len f;
B3: ( len f >= i & i >= 1 ) by B1, FINSEQ_3:25;
then reconsider k = (len f) - i as Element of NAT by NAT_1:21;
( k + i >= k + 1 & 1 + k >= 1 + 0 ) by B3, XREAL_1:6;
then k + 1 in dom f by FINSEQ_3:25;
then f . (k + 1) = f . i by B1, FUNCT_1:def 10;
hence (Rev f) . i = f . i by B2, FINSEQ_5:def 3; :: thesis: verum

end;

hence Rev f = f by A1, FUNCT_1:2; :: thesis: verum