set X = HFuncs NAT;
thus ( 0 const 0 in HFuncs NAT & 1 succ 1 in HFuncs NAT & ( for n, i being Nat st 1 <= i & i <= n holds
n proj i in HFuncs NAT ) ) by Th30, Th32, Th34; :: according to COMPUT_1:def 14 :: thesis: ( HFuncs NAT is composition_closed & HFuncs NAT is primitive-recursion_closed )
thus for f being Element of HFuncs NAT
for F being with_the_same_arity FinSequence of HFuncs NAT st f in HFuncs NAT & arity f = len F & rng F c= HFuncs NAT holds
f * <:F:> in HFuncs NAT by Th41; :: according to COMPUT_1:def 12 :: thesis: HFuncs NAT is primitive-recursion_closed
let g be Element of HFuncs NAT; :: according to COMPUT_1:def 13 :: thesis: for f1, f2 being Element of HFuncs NAT
for i being Nat st g is_primitive-recursively_expressed_by f1,f2,i & f1 in HFuncs NAT & f2 in HFuncs NAT holds
g in HFuncs NAT
thus for f1, f2 being Element of HFuncs NAT
for i being Nat st g is_primitive-recursively_expressed_by f1,f2,i & f1 in HFuncs NAT & f2 in HFuncs NAT holds
g in HFuncs NAT ; :: thesis: verum