theorem Th97: :: FINSEQ_2:99

for D being non empty set holds 2 -tuples_on D = { <*d1,d2*> where d1, d2 is Element of D : verum }