take n |-> 1 ; :: thesis: ( n |-> 1 is positive-yielding & n |-> 1 is natural-valued & n |-> 1 is n -element )
thus ( n |-> 1 is positive-yielding & n |-> 1 is natural-valued & n |-> 1 is n -element ) ; :: thesis: verum