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