theorem Th30: :: COMPUT_1:31

for m, n being Nat holds n const m in HFuncs NAT