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