theorem Th35: :: COMPUT_1:36

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