for i, n being Element of NAT holds
( dom (n proj i) = n -tuples_on NAT & ( 1 <= i & i <= n implies rng (n proj i) = NAT ) )