theorem Th34: :: COMPUT_1:35

for i, n being Nat holds n proj i in HFuncs NAT