let D be non empty set ; :: thesis: for d being XFinSequence of D holds rng d = rng (XFS2FS d)
let d be XFinSequence of D; :: thesis: rng d = rng (XFS2FS d)
set Xd = XFS2FS d;
A1: len (XFS2FS d) = len d by AFINSQ_1:def 9;
thus rng d c= rng (XFS2FS d) :: according to XBOOLE_0:def 10 :: thesis: rng (XFS2FS d) c= rng d

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng d or y in rng (XFS2FS d) )
assume y in rng d ; :: thesis: y in rng (XFS2FS d)
then consider x being object such that
A2: x in dom d and
A3: d . x = y by FUNCT_1:def 3;
reconsider x = x as Nat by A2;
A4: (x + 1) -' 1 = x by NAT_D:34;
A5: x + 1 <= len d by A2, AFINSQ_1:66, NAT_1:13;
then A6: d . x = (XFS2FS d) . (x + 1) by NAT_1:11, A4, AFINSQ_1:def 9;
x + 1 in dom (XFS2FS d) by A1, NAT_1:11, A5, FINSEQ_3:25;
hence y in rng (XFS2FS d) by A6, A3, FUNCT_1:def 3; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (XFS2FS d) or y in rng d )
assume y in rng (XFS2FS d) ; :: thesis: y in rng d
then consider x being object such that
A7: x in dom (XFS2FS d) and
A8: (XFS2FS d) . x = y by FUNCT_1:def 3;
reconsider x = x as Nat by A7;
A9: 1 <= x by A7, FINSEQ_3:25;
A10: x <= len (XFS2FS d) by A7, FINSEQ_3:25;
x - 1 >= 1 - 1 by A7, FINSEQ_3:25, XREAL_1:9;
then A11: x - 1 = x -' 1 by XREAL_0:def 2;
A12: d . (x -' 1) = (XFS2FS d) . x by A9, A10, A1, AFINSQ_1:def 9;
(x -' 1) + 1 = x by A11;
then x -' 1 in dom d by A10, A1, NAT_1:13, AFINSQ_1:66;
hence y in rng d by A8, A12, FUNCT_1:def 3; :: thesis: verum