let D be set ; :: thesis: for p being FinSequence of D
for n being Nat holds
( n + 1 in dom p iff n in dom (FS2XFS p) )
let p be FinSequence of D; :: thesis: for n being Nat holds
( n + 1 in dom p iff n in dom (FS2XFS p) )
let n be Nat; :: thesis: ( n + 1 in dom p iff n in dom (FS2XFS p) )

hereby :: thesis: ( n in dom (FS2XFS p) implies n + 1 in dom p )

assume n + 1 in dom p ; :: thesis: n in dom (FS2XFS p)
then n + 1 <= len p by FINSEQ_3:25;
then (n + 1) - 1 < (len p) - 0 by XREAL_1:15;
then n < len (FS2XFS p) by Def8;
then n in Segm (dom (FS2XFS p)) by NAT_1:44;
hence n in dom (FS2XFS p) ; :: thesis: verum

end;

assume n in dom (FS2XFS p) ; :: thesis: n + 1 in dom p
then n in Segm (dom (FS2XFS p)) ;
then ( 0 <= n & n < len (FS2XFS p) ) by NAT_1:44;
then ( 0 + 1 <= n + 1 & n < len p ) by Def8, XREAL_1:6;
then ( 1 <= n + 1 & n + 1 <= len p ) by NAT_1:13;
hence n + 1 in dom p by FINSEQ_3:25; :: thesis: verum