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