theorem SFF: :: RVSUM_4:43

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