let D be non empty set ; :: thesis: for z being Tuple of 1,D ex d being Element of D st z = <*d*>
let z be Tuple of 1,D; :: thesis: ex d being Element of D st z = <*d*>
z in 1 -tuples_on D by Lm6;
then z in { <*d*> where d is Element of D : verum } by Th94;
hence ex d being Element of D st z = <*d*> ; :: thesis: verum