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: for Y being set st Y in { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } holds
0 const 0 in Y

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

end;

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

proof

thus 0 const 0 in PrimRec by A2, A3, SETFAM_1:def 1; :: according to COMPUT_1:def 14 :: thesis: ( 1 succ 1 in PrimRec & ( for n, i being Nat st 1 <= i & i <= n holds
n proj i in PrimRec ) & PrimRec is composition_closed & PrimRec is primitive-recursion_closed )

now :: thesis: for Y being set st Y in { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } holds
1 succ 1 in Y

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

end;

hence 1 succ 1 in PrimRec by A2, SETFAM_1:def 1; :: thesis: ( ( for n, i being Nat st 1 <= i & i <= n holds
n proj i in PrimRec ) & PrimRec is composition_closed & PrimRec is primitive-recursion_closed )

hereby :: thesis: ( PrimRec is composition_closed & PrimRec is primitive-recursion_closed )

let n, i be Nat; :: thesis: ( 1 <= i & i <= n implies n proj i in PrimRec )
assume that
A4: 1 <= i and
A5: i <= n ; :: thesis: n proj i in PrimRec

now :: thesis: for Y being set st Y in { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } holds
n proj i in Y

let Y be set ; :: thesis: ( Y in { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } implies n proj i in Y )
assume Y in { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } ; :: thesis: n proj i in Y
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: verum

end;

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

end;

hereby :: according to COMPUT_1:def 12 :: thesis: PrimRec is primitive-recursion_closed

let f be Element of HFuncs NAT; :: thesis: for F being with_the_same_arity FinSequence of HFuncs NAT st f in PrimRec & arity f = len F & rng F c= PrimRec holds
f * <:F:> in PrimRec
let F be with_the_same_arity FinSequence of HFuncs NAT; :: thesis: ( f in PrimRec & arity f = len F & rng F c= PrimRec implies f * <:F:> in PrimRec )
assume that
A6: f in PrimRec and
A7: arity f = len F and
A8: rng F c= PrimRec ; :: thesis: f * <:F:> in PrimRec

now :: thesis: for Y being set st Y in { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } holds
f * <:F:> in Y

let Y be set ; :: thesis: ( Y in { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } implies f * <:F:> in Y )
assume A9: Y in { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } ; :: thesis: f * <:F:> in Y
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: verum

end;

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

end;

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

let g, f1, f2 be Element of HFuncs NAT; :: thesis: for i being Nat st g is_primitive-recursively_expressed_by f1,f2,i & f1 in PrimRec & f2 in PrimRec holds
g in PrimRec
let i be Nat; :: thesis: ( g is_primitive-recursively_expressed_by f1,f2,i & f1 in PrimRec & f2 in PrimRec implies g in PrimRec )
assume that
A14: g is_primitive-recursively_expressed_by f1,f2,i and
A15: f1 in PrimRec and
A16: f2 in PrimRec ; :: thesis: g in PrimRec

now :: thesis: for Y being set st Y in { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } holds
g in Y

let Y be set ; :: thesis: ( Y in { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } implies g in Y )
assume A17: Y in { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } ; :: thesis: g in Y
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: verum

end;

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

end;

end;