theorem Th103: :: FINSEQ_2:105

for i, j being natural Number
for D being non empty set holds (i + j) -tuples_on D = { (z ^ t) where z is Tuple of i,D, t is Tuple of j,D : verum }