let k, n be Nat; :: thesis: ( 1 <= n & n <= k implies k succ n in k -aryPrimRecFuncs )
assume A1: ( 1 <= n & n <= k ) ; :: thesis: k succ n in k -aryPrimRecFuncs
set f = k succ n;
A2: k succ n in HFuncs NAT by COMPUT_1:33;
A3: k succ n is k -ary

proof

thus arity (k succ n) = k ; :: according to COMPUT_1:def 21 :: thesis: verum

end;

k succ n is primitive-recursive

proof

thus k succ n in PrimRec by A1, COMPUT_1:70; :: according to COMPUT_1:def 16 :: thesis: verum

end;

hence k succ n in k -aryPrimRecFuncs by A2, A3; :: thesis: verum