theorem Th37: :: COMPUT_1:38

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