let n be Nat; :: thesis: for f being XFinSequence st n in dom (XFS2FS f) holds
n - 1 in dom f
let f be XFinSequence; :: thesis: ( n in dom (XFS2FS f) implies n - 1 in dom f )
set g = XFS2FS f;
assume A1: n in dom (XFS2FS f) ; :: thesis: n - 1 in dom f
then reconsider n = n as non zero Nat by FINSEQ_3:25;
A2: len (XFS2FS f) = len f by AFINSQ_1:def 9;
n <= len (XFS2FS f) by A1, FINSEQ_3:25;
then n - 1 < (len f) - 0 by A2, XREAL_1:8;
hence n - 1 in dom f by AFINSQ_1:86; :: thesis: verum