dom (p +* (i,k)) = dom p by FUNCT_7:30;
then len (p +* (i,k)) = len p by FINSEQ_3:29
.= n by CARD_1:def 7 ;
hence p +* (i,k) is Element of n -tuples_on NAT by FINSEQ_2:92; :: thesis: verum