set p = XFS2FS q;
A1:
len (XFS2FS q) = len q
by Def9A;
rng (XFS2FS q) c= D
proof
let y be
object ;
TARSKI:def 3 ( not y in rng (XFS2FS q) or y in D )
A3:
rng q c= D
by RELAT_1:def 19;
assume
y in rng (XFS2FS q)
;
y in D
then consider x being
object such that A4:
x in dom (XFS2FS q)
and A5:
y = (XFS2FS q) . x
by FUNCT_1:def 3;
reconsider nx =
x as
Element of
NAT by A4;
A6:
nx in Seg (len q)
by A1, A4, FINSEQ_1:def 3;
then f:
1
<= nx
by FINSEQ_1:1;
then
nx - 1
>= 0
by XREAL_1:48;
then A7:
nx - 1
= nx -' 1
by XREAL_0:def 2;
A8:
nx - 1
< (nx - 1) + 1
by A7, NAT_1:13;
F:
nx <= len q
by A6, FINSEQ_1:1;
then
nx - 1
< len q
by A8, XXREAL_0:2;
then a9:
nx - 1
in dom q
by A7, Lm1;
AA:
( 1
<= nx &
nx <= len q )
by F, f;
A9:
q . (nx - 1) in rng q
by FUNCT_1:def 3, a9;
(XFS2FS q) . nx = q . (nx - 1)
by Def9A, AA;
hence
y in D
by A5, A9, A3;
verum
end;
hence
XFS2FS q is FinSequence of D
by FINSEQ_1:def 4; verum