theorem SXX: :: RVSUM_4:45

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