reconsider p = id (Seg n) as FinSequence by FINSEQ_2:48;

len p = len (idseq n) by FINSEQ_2:def 1

.= n by CARD_1:def 7 ;

then reconsider p = p as FinSeqLen of n by CARD_1:def 7;

take p ; :: thesis: ( p is one-to-one & p is nonpair-yielding )

thus p is one-to-one ; :: thesis: p is nonpair-yielding

let x be set ; :: according to FACIRC_1:def 3 :: thesis: ( x in dom p implies not p . x is pair )

assume A1: x in dom p ; :: thesis: not p . x is pair

x in Seg n by A1;

hence not p . x is pair by FUNCT_1:17; :: thesis: verum

len p = len (idseq n) by FINSEQ_2:def 1

.= n by CARD_1:def 7 ;

then reconsider p = p as FinSeqLen of n by CARD_1:def 7;

take p ; :: thesis: ( p is one-to-one & p is nonpair-yielding )

thus p is one-to-one ; :: thesis: p is nonpair-yielding

let x be set ; :: according to FACIRC_1:def 3 :: thesis: ( x in dom p implies not p . x is pair )

assume A1: x in dom p ; :: thesis: not p . x is pair

x in Seg n by A1;

hence not p . x is pair by FUNCT_1:17; :: thesis: verum