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