let D be set ; :: thesis: for p being FinSequence of D holds rng p = rng (FS2XFS p)
let p be FinSequence of D; :: thesis: rng p = rng (FS2XFS p)
for y being object holds
( y in rng (FS2XFS p) iff ex x being object st
( x in dom p & p . x = y ) )

proof

let y be object ; :: thesis: ( y in rng (FS2XFS p) iff ex x being object st
( x in dom p & p . x = y ) )
thus ( y in rng (FS2XFS p) implies ex x being object st
( x in dom p & p . x = y ) ) :: thesis: ( ex x being object st
( x in dom p & p . x = y ) implies y in rng (FS2XFS p) )

proof

assume y in rng (FS2XFS p) ; :: thesis: ex x being object st
( x in dom p & p . x = y )
then consider n being object such that
A1: ( n in dom (FS2XFS p) & (FS2XFS p) . n = y ) by FUNCT_1:def 3;
reconsider n = n as Nat by A1;
take n + 1 ; :: thesis: ( n + 1 in dom p & p . (n + 1) = y )
thus n + 1 in dom p by A1, Th13; :: thesis: p . (n + 1) = y
n < len (FS2XFS p) by A1, Lm1;
then n < len p by Def8;
hence p . (n + 1) = y by A1, Def8; :: thesis: verum

end;

given x being object such that A2: ( x in dom p & p . x = y ) ; :: thesis: y in rng (FS2XFS p)
reconsider n1 = x as Nat by A2;
A3: ( 1 <= n1 & n1 <= len p ) by A2, FINSEQ_3:25;
then reconsider n = n1 - 1 as Nat by Th0;
n < (len p) - 0 by A3, XREAL_1:15;
then A4: p . (n + 1) = (FS2XFS p) . n by Def8;
n + 1 in dom p by A2;
then n in dom (FS2XFS p) by Th13;
hence y in rng (FS2XFS p) by A2, A4, FUNCT_1:3; :: thesis: verum

end;

hence rng p = rng (FS2XFS p) by FUNCT_1:def 3; :: thesis: verum