theorem Th5: :: BALLOT_1:5

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