theorem Th17: :: FINSEQ_1:17

for a being natural Number
for p, q being FinSequence st a <= len p & q = p | (Seg a) holds
( len q = a & dom q = Seg a )