consider p being one-to-one FinSequence of NAT ;
take p ; :: thesis: ( p is one-to-one & p is natural-valued )
thus ( p is one-to-one & p is natural-valued ) ; :: thesis: verum