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