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