<*d*> in 1 -tuples_on D by FINSEQ_2:98;
hence <*d*> is Tuple of 1,D ; :: thesis: verum