theorem :: FINSEQ_3:130

for D being non empty set holds product <*D,D,D*> = 3 -tuples_on D