theorem Th18: :: FINSEQ_1:18

for a being natural Number
for D being set
for p being b₂ -valued FinSequence holds p | (Seg a) is FinSequence of D