theorem FXF: :: RVSUM_4:40

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