for D being set
for p being XFinSequence of D holds FS2XFS (XFS2FS p) = p