set p = id (Seg n);
A1: ( dom (id (Seg n)) = Seg n & rng (id (Seg n)) = Seg n ) by RELAT_1:71;
then id (Seg n) is FinSequence by FINSEQ_1:def 2;
then reconsider p = id (Seg n) as one-to-one FinSequence of NAT by A1, FINSEQ_1:def 4;
len p = n by A1, FINSEQ_1:def 3;
then reconsider p = p as FinSeqLen of by FINSEQ_1:def 18;
take p ; :: thesis: ( p is one-to-one & p is natural-valued )
thus ( p is one-to-one & p is natural-valued ) ; :: thesis: verum