let k, n be Nat; :: thesis: k const n in k -aryPrimRecFuncs
k const n in HFuncs NAT by COMPUT_1:31;
hence k const n in k -aryPrimRecFuncs ; :: thesis: verum