for D being set
for p being FinSequence of D
for n being Nat holds
( (FS2XFS p) | n = FS2XFS (p | n) & (FS2XFS p) /^ n = FS2XFS (p /^ n) )