for D being set
for d being FinSequence of D holds XFS2FS (FS2XFS d) = d ;