theorem Th46: :: FINSEQ_2:48

for k being natural Number holds id (Seg k) is FinSequence of NAT