theorem Th1: :: BALLOT_1:1

for D being non empty set
for d being XFinSequence of D
for n being Nat holds XFS2FS (d | n) = (XFS2FS d) | n by AFINSQ_2:84;