let k be natural Number ; :: thesis: id (Seg k) is FinSequence of NAT
set I = id (Seg k);
reconsider k = k as Element of NAT by ORDINAL1:def 12;
dom (id (Seg k)) = Seg k ;
then ( rng (id (Seg k)) = Seg k & id (Seg k) is FinSequence ) by FINSEQ_1:def 2;
hence id (Seg k) is FinSequence of NAT by FINSEQ_1:def 4; :: thesis: verum