for D being set
for f being FinSequence of D
for g being XFinSequence of D holds FS2XFS (f ^ g) = (FS2XFS f) ^ g