let f be XFinSequence; :: thesis: ( dom f = dom (Rev f) & rng f = rng (Rev f) )
thus A1: dom f = len f
.= len (Rev f) by Def3
.= dom (Rev f) ; :: 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 set ; :: thesis: ( x in rng f implies x in rng (Rev f) )
assume x in rng f ; :: thesis: x in rng (Rev f)
then consider z being set such that
A3: z in dom f and
A4: f . z = x by FUNCT_1:def 5;
reconsider i = z as Element of NAT by A3;
i < len f by A3, NAT_1:45;
then i + 1 <= len f by NAT_1:13;
then (len f) -' (i + 1) = (len f) - (i + 1) by XREAL_1:235;
then reconsider j = (len f) - (i + 1) as Element of NAT ;
(len f) - (i + 1) < len f by XREAL_1:46;
then A5: j in len (Rev f) by A2, NAT_1:45;
then (Rev f) . j = f . ((len f) - (j + 1)) by Def3;
hence x in rng (Rev f) by A4, A5, FUNCT_1:def 5; :: thesis: verum

end;

let x be set ; :: 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 z being set such that
A6: z in dom (Rev f) and
A7: (Rev f) . z = x by FUNCT_1:def 5;
reconsider i = z as Element of NAT by A6;
A8: (Rev f) . i = f . ((len f) - (i + 1)) by A6, Def3;
i < len f by A2, A6, NAT_1:45;
then i + 1 <= len f by NAT_1:13;
then (len f) -' (i + 1) = (len f) - (i + 1) by XREAL_1:235;
then reconsider j = (len f) - (i + 1) as Element of NAT ;
(len f) - (i + 1) < len f by XREAL_1:46;
then j in len (Rev f) by A2, NAT_1:45;
hence x in rng f by A1, A7, A8, FUNCT_1:def 5; :: thesis: verum