theorem Th12: :: AFINSQ_1:93

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