let D be non empty set ; :: thesis: product <*D,D,D*> = 3 -tuples_on D
thus product <*D,D,D*> = { <*d1,d2,d3*> where d1, d2, d3 is Element of D : verum } by Th127
.= 3 -tuples_on D by FINSEQ_2:102 ; :: thesis: verum