theorem XFX: :: RVSUM_4:39

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