for i, n being Element of NAT
for t being Element of n -tuples_on NAT holds (n proj i) . t = t . i