set S = { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } ;
A1: {(HFuncs NAT)} c= bool (HFuncs NAT) by ZFMISC_1:68;
HFuncs NAT in {(HFuncs NAT)} by TARSKI:def 1;
then A2: HFuncs NAT in { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } by A1, Th65;

A3: now :: thesis:

let Y be set ; :: thesis:
assume Y in { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } ; :: thesis:
then ex R being Subset of (HFuncs NAT) st
( R = Y & R is primitive-recursively_closed ) ;
hence 0 const 0 in Y ; :: thesis:

end;

hence not PrimRec is empty by A2, SETFAM_1:def 1; :: thesis:
thus PrimRec is primitive-recursively_closed :: thesis:

proof

thus 0 const 0 in PrimRec by A2, A3, SETFAM_1:def 1; :: according to COMPUT_1:def 14 :: thesis:

now :: thesis:

let Y be set ; :: thesis:
assume Y in { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } ; :: thesis:
then ex R being Subset of (HFuncs NAT) st
( R = Y & R is primitive-recursively_closed ) ;
hence 1 succ 1 in Y ; :: thesis:

end;

hence 1 succ 1 in PrimRec by A2, SETFAM_1:def 1; :: thesis:

hereby :: thesis:

let n, i be Element of NAT ; :: thesis:
assume that
A4: 1 <= i and
A5: i <= n ; :: thesis:

now :: thesis:

let Y be set ; :: thesis:
assume Y in { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } ; :: thesis:
then ex R being Subset of (HFuncs NAT) st
( R = Y & R is primitive-recursively_closed ) ;
hence n proj i in Y by A4, A5; :: thesis:

end;

hence n proj i in PrimRec by A2, SETFAM_1:def 1; :: thesis:

end;

hereby :: according to COMPUT_1:def 12 :: thesis:

let f be Element of HFuncs NAT; :: thesis:
let F be with_the_same_arity FinSequence of HFuncs NAT; :: thesis:
assume that
A6: f in PrimRec and
A7: arity f = len F and
A8: rng F c= PrimRec ; :: thesis:

now :: thesis:

let Y be set ; :: thesis:
assume A9: Y in { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } ; :: thesis:
then consider R being Subset of (HFuncs NAT) such that
A10: R = Y and
A11: R is primitive-recursively_closed ;
A12: R is composition_closed by A11;
A13: PrimRec c= R by A9, A10, SETFAM_1:3;
then rng F c= R by A8;
hence f * <:F:> in Y by A6, A7, A10, A12, A13; :: thesis:

end;

hence f * <:F:> in PrimRec by A2, SETFAM_1:def 1; :: thesis:

end;

hereby :: according to COMPUT_1:def 13 :: thesis:

let g, f1, f2 be Element of HFuncs NAT; :: thesis:
let i be Element of NAT ; :: thesis:
assume that
A14: g is_primitive-recursively_expressed_by f1,f2,i and
A15: f1 in PrimRec and
A16: f2 in PrimRec ; :: thesis:

now :: thesis:

let Y be set ; :: thesis:
assume A17: Y in { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } ; :: thesis:
then consider R being Subset of (HFuncs NAT) such that
A18: R = Y and
A19: R is primitive-recursively_closed ;
A20: f2 in R by A16, A17, A18, SETFAM_1:def 1;
A21: R is primitive-recursion_closed by A19;
f1 in R by A15, A17, A18, SETFAM_1:def 1;
hence g in Y by A14, A18, A21, A20; :: thesis:

end;

hence g in PrimRec by A2, SETFAM_1:def 1; :: thesis:

end;

end;