:: deftheorem Def16 defines constF ACKERMAN:def 16 :
for m being Nat
for b₂ being Function of NAT,(HFuncs NAT) holds
( b₂ = constF m iff for n being Nat holds b₂ . n = m const n );