thus p +* (i,k) is Element of n -tuples_on NAT ; :: thesis: verum