theorem Th54: :: FINSEQ_2:56

for a being object
for k being natural Number holds (Seg k) --> a is FinSequence