theorem Th15: :: FINSEQ_1:15

for a being natural Number
for p being FinSequence holds p | (Seg a) is FinSequence