set n = the Nat;

set p = the one-to-one nonpair-yielding FinSeqLen of the Nat;

take the one-to-one nonpair-yielding FinSeqLen of the Nat ; :: thesis: ( the one-to-one nonpair-yielding FinSeqLen of the Nat is one-to-one & the one-to-one nonpair-yielding FinSeqLen of the Nat is nonpair-yielding )

thus ( the one-to-one nonpair-yielding FinSeqLen of the Nat is one-to-one & the one-to-one nonpair-yielding FinSeqLen of the Nat is nonpair-yielding ) ; :: thesis: verum

set p = the one-to-one nonpair-yielding FinSeqLen of the Nat;

take the one-to-one nonpair-yielding FinSeqLen of the Nat ; :: thesis: ( the one-to-one nonpair-yielding FinSeqLen of the Nat is one-to-one & the one-to-one nonpair-yielding FinSeqLen of the Nat is nonpair-yielding )

thus ( the one-to-one nonpair-yielding FinSeqLen of the Nat is one-to-one & the one-to-one nonpair-yielding FinSeqLen of the Nat is nonpair-yielding ) ; :: thesis: verum