let p be XFinSequence; :: thesis: ( dom p = dom (Rev p) & rng p = rng (Rev p) )
thus A1: dom p = len p
.= len (Rev p) by Def1
.= dom (Rev p) ; :: thesis: rng p = rng (Rev p)
A2: len p = len (Rev p) by Def1;
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: rng (Rev p) c= rng p
let x be object ; :: thesis: ( x in rng p implies x in rng (Rev p) )
assume x in rng p ; :: thesis: x in rng (Rev p)
then consider z being object such that
A3: z in dom p and
A4: p . z = x by FUNCT_1:def 3;
reconsider i = z as Element of NAT by A3;
i + 1 <= len p by NAT_1:13, A3, AFINSQ_1:86;
then (len p) -' (i + 1) = (len p) - (i + 1) by XREAL_1:233;
then reconsider j = (len p) - (i + 1) as Element of NAT ;
A5: j in len (Rev p) by A2, AFINSQ_1:86, XREAL_1:44;
then (Rev p) . j = p . ((len p) - (j + 1)) by Def1;
hence x in rng (Rev p) 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 p) or x in rng p )
assume x in rng (Rev p) ; :: thesis: x in rng p
then consider z being object such that
A6: z in dom (Rev p) and
A7: (Rev p) . z = x by FUNCT_1:def 3;
reconsider i = z as Element of NAT by A6;
i < len p by A2, A6, AFINSQ_1:86;
then i + 1 <= len p by NAT_1:13;
then (len p) -' (i + 1) = (len p) - (i + 1) by XREAL_1:233;
then reconsider j = (len p) - (i + 1) as Element of NAT ;
(len p) - (i + 1) < len p by XREAL_1:44;
then A8: j in len (Rev p) by A2, AFINSQ_1:86;
(Rev p) . i = p . ((len p) - (i + 1)) by A6, Def1;
hence x in rng p by A1, A7, A8, FUNCT_1:def 3; :: thesis: verum