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