theorem :: FINSEQ_3:126

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