theorem FFX: :: RVSUM_4:41

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