theorem Th32: :: COMPUT_1:33

for i, n being Nat holds n succ i in HFuncs NAT