consider n being Nat, p being one-to-one nonpair-yielding FinSeqLen of n;
take p ; :: thesis: ( p is one-to-one & p is nonpair-yielding )
thus ( p is one-to-one & p is nonpair-yielding ) ; :: thesis: verum