let x be object ; :: thesis: Rev <*x*> = <*x*>
set f = <*x*>;
A1: len <*x*> = 1 by FINSEQ_1:39;

now :: thesis: for i being Nat st i in dom <*x*> holds
<*x*> . i = <*x*> . (((len <*x*>) - i) + 1)

let i be Nat; :: thesis: ( i in dom <*x*> implies <*x*> . i = <*x*> . (((len <*x*>) - i) + 1) )
assume i in dom <*x*> ; :: thesis: <*x*> . i = <*x*> . (((len <*x*>) - i) + 1)
then i in Seg (len <*x*>) by FINSEQ_1:def 3;
then i = 1 by A1, FINSEQ_1:2, TARSKI:def 1;
hence <*x*> . i = <*x*> . (((len <*x*>) - i) + 1) by FINSEQ_1:39; :: thesis: verum

end;

hence Rev <*x*> = <*x*> by Def3; :: thesis: verum