theorem SSX: :: RVSUM_4:46

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