theorem :: FINSEQ_2:107

for i, j being natural Number
for D being non empty set
for z being Tuple of i,D
for t being Tuple of j,D holds z ^ t is Tuple of i + j,D ;