theorem Th30: :: COMPUT_1:31

for m, n being Element of NAT holds n const m in HFuncs NAT