reconsider i = i, k = k as Element of NAT by ORDINAL1:def 12;
p +* (i,k) is Element of n -tuples_on NAT ;
hence p +* (i,k) is Element of n -tuples_on NAT ; :: thesis: verum