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