let D be non empty set ; :: thesis: product <*D*> = 1 -tuples_on D
<*D*> = 1 |-> D by FINSEQ_2:59
.= (Seg 1) --> D ;
then product <*D*> = Funcs ((Seg 1),D) by CARD_3:11;
hence product <*D*> = 1 -tuples_on D by FINSEQ_2:93; :: thesis: verum