dom (p +* i,k) = dom p by FUNCT_7:32;
then len (p +* i,k) = len p by FINSEQ_3:31
.= n by FINSEQ_1:def 18 ;
hence p +* i,k is Element of n -tuples_on NAT by FINSEQ_2:110; :: thesis: verum