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

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

assume n in dom p ; :: thesis: n + 1 in dom (XFS2FS p)
then n in dom (FS2XFS (XFS2FS p)) ;
hence n + 1 in dom (XFS2FS p) by Th13; :: thesis: verum

end;

assume n + 1 in dom (XFS2FS p) ; :: thesis: n in dom p
then n in dom (FS2XFS (XFS2FS p)) by Th13;
hence n in dom p ; :: thesis: verum