theorem Th36: :: COMPUT_1:37
for i, n being Element of NAT holds arity (n proj i) = n