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