set p = the one-to-one FinSequence of NAT ;
take the one-to-one FinSequence of NAT ; :: thesis: ( the one-to-one FinSequence of NAT is one-to-one & the one-to-one FinSequence of NAT is natural-valued )
thus ( the one-to-one FinSequence of NAT is one-to-one & the one-to-one FinSequence of NAT is natural-valued ) ; :: thesis: verum