theorem Th34: :: COMPUT_1:35

for i, n being Element of NAT holds n proj i in HFuncs NAT