take n |-> the Element of D ; :: thesis: ( n |-> the Element of D is n -element & n |-> the Element of D is D -valued )
thus ( n |-> the Element of D is n -element & n |-> the Element of D is D -valued ) ; :: thesis: verum