theorem Th17: :: AFINSQ_2:84

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