reconsider p = id (Seg n) as FinSequence by FINSEQ_2:52;
len p = len (idseq n) by FINSEQ_2:def 1
.= n by FINSEQ_1:def 18 ;
then reconsider p = p as FinSeqLen of by FINSEQ_1:def 18;
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
then A2: x in Seg n by RELAT_1:71;
reconsider i = x as Element of NAT by A1;
p . x = i by A2, FUNCT_1:34;
hence not p . x is pair ; :: thesis: verum