( p is Tuple of k, & q is Tuple of n, ) by FINSEQ_2:151;
then p ^ q is Tuple of k + n, by FINSEQ_2:127;
hence p ^ q is Element of (k + n) -tuples_on D by FINSEQ_2:151; :: thesis: verum