for D being set
for p being XFinSequence of D
for n being Nat holds
( n in dom p iff n + 1 in dom (XFS2FS p) )