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