theorem Th5: :: AFINSQ_2:85

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