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

A2: now

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 consider R being Subset of (HFuncs NAT ) such that
A3: ( R = Y & R is primitive-recursively_closed ) ;
thus 0 const 0 in Y by A3, Def17; :: thesis: verum

end;

hence not PrimRec is empty by A1, 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 A1, A2, SETFAM_1:def 1; :: according to COMPUT_1:def 17 :: thesis: ( 1 succ 1 in PrimRec & ( for n, i being Element of NAT st 1 <= i & i <= n holds
n proj i in PrimRec ) & PrimRec is composition_closed & PrimRec is primitive-recursion_closed )

now

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 consider R being Subset of (HFuncs NAT ) such that
A4: ( R = Y & R is primitive-recursively_closed ) ;
thus 1 succ 1 in Y by A4, Def17; :: thesis: verum

end;

hence 1 succ 1 in PrimRec by A1, SETFAM_1:def 1; :: thesis: ( ( for n, i being Element of 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 Element of NAT ; :: thesis: ( 1 <= i & i <= n implies n proj i in PrimRec )
assume A5: ( 1 <= i & i <= n ) ; :: thesis: n proj i in PrimRec

now

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 consider R being Subset of (HFuncs NAT ) such that
A6: ( R = Y & R is primitive-recursively_closed ) ;
thus n proj i in Y by A5, A6, Def17; :: thesis: verum

end;

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

end;

hereby :: according to COMPUT_1:def 15 :: 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 A7: ( f in PrimRec & arity f = len F & rng F c= PrimRec ) ; :: thesis: f * <:F:> in PrimRec

now

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 A8: 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
A9: ( R = Y & R is primitive-recursively_closed ) ;
A10: R is composition_closed by A9, Def17;
PrimRec c= R by A8, A9, SETFAM_1:4;
then ( f in R & rng F c= R ) by A7, XBOOLE_1:1;
hence f * <:F:> in Y by A7, A9, A10, Def15; :: thesis: verum

end;

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

end;

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

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

now

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 A14: 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
A15: ( R = Y & R is primitive-recursively_closed ) ;
A16: R is primitive-recursion_closed by A15, Def17;
( f1 in R & f2 in R ) by A12, A13, A14, A15, SETFAM_1:def 1;
hence g in Y by A11, A15, A16, Def16; :: thesis: verum

end;

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

end;

end;