theorem Th27: :: COMPUT_1:28

for f being NAT * -defined to-naturals homogeneous Function holds f is Element of HFuncs NAT