theorem XFF: :: RVSUM_4:42

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