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