theorem Th104: :: FINSEQ_2:106

for i, j being natural Number
for D being non empty set
for s being Tuple of i + j,D ex z being Element of i -tuples_on D ex t being Element of j -tuples_on D st s = z ^ t