let f be FinSequence; :: thesis: ( dom f = dom (Rev f) & rng f = rng (Rev f) )
thus A1: dom f = Seg (len f) by FINSEQ_1:def 3
.= Seg (len (Rev f)) by Def3
.= dom (Rev f) by FINSEQ_1:def 3 ; :: thesis: rng f = rng (Rev f)
A2: len f = len (Rev f) by Def3;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: rng (Rev f) c= rng f

let x be object ; :: thesis: ( x in rng f implies x in rng (Rev f) )
assume x in rng f ; :: thesis: x in rng (Rev f)
then consider i being Nat such that
A3: i in dom f and
A4: f . i = x by FINSEQ_2:10;
i <= len f by A3, FINSEQ_3:25;
then reconsider j = ((len f) - i) + 1 as Element of NAT by Th1;
dom f = Seg (len f) by FINSEQ_1:def 3;
then j in Seg (len (Rev f)) by A2, A3, Th2;
then A5: j in dom (Rev f) by FINSEQ_1:def 3;
then (Rev f) . j = f . (((len f) - j) + 1) by Def3;
hence x in rng (Rev f) by A4, A5, FUNCT_1:def 3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (Rev f) or x in rng f )
assume x in rng (Rev f) ; :: thesis: x in rng f
then consider i being Nat such that
A6: i in dom (Rev f) and
A7: (Rev f) . i = x by FINSEQ_2:10;
i <= len f by A2, A6, FINSEQ_3:25;
then reconsider j = ((len f) - i) + 1 as Element of NAT by Th1;
i in Seg (len (Rev f)) by A6, FINSEQ_1:def 3;
then j in Seg (len (Rev f)) by A2, Th2;
then A8: j in dom (Rev f) by FINSEQ_1:def 3;
(Rev f) . i = f . (((len f) - i) + 1) by A6, Def3;
hence x in rng f by A1, A7, A8, FUNCT_1:def 3; :: thesis: verum