let f be FinSequence; :: thesis: Rev (Rev f) = f
A1: len f = len (Rev f) by FINSEQ_5:def 3;

now

let i be Nat; :: thesis: ( i in dom f implies f . i = (Rev f) . (((len (Rev f)) - i) + 1) )
assume A2: i in dom f ; :: thesis: f . i = (Rev f) . (((len (Rev f)) - i) + 1)
then i in dom (Rev f) by FINSEQ_5:57;
then i <= len (Rev f) by FINSEQ_3:25;
then reconsider j = (len (Rev f)) - i as Element of NAT by INT_1:5;
(j + 1) + i = (len (Rev f)) + 1 ;
then A3: j + 1 in dom (Rev f) by A1, A2, FINSEQ_5:59;
thus f . i = f . (((len f) - (((len (Rev f)) - i) + 1)) + 1) by A1
.= (Rev f) . (((len (Rev f)) - i) + 1) by A3, FINSEQ_5:def 3 ; :: thesis: verum

end;

hence Rev (Rev f) = f by A1, FINSEQ_5:def 3; :: thesis: verum