theorem :: BALLOT_1:5

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