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

A3: now

let Y be set ; :: thesis: ( Y in { R where R is Subset of : R is primitive-recursively_closed } implies 0 const 0 in Y )
assume Y in { R where R is Subset of : R is primitive-recursively_closed } ; :: thesis: 0 const 0 in Y
then ex R being Subset of st
( R = Y & R is primitive-recursively_closed ) ;
hence 0 const 0 in Y by Def17; :: 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 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 : R is primitive-recursively_closed } implies 1 succ 1 in Y )
assume Y in { R where R is Subset of : R is primitive-recursively_closed } ; :: thesis: 1 succ 1 in Y
then ex R being Subset of st
( R = Y & R is primitive-recursively_closed ) ;
hence 1 succ 1 in Y by Def17; :: thesis: verum

end;

hence 1 succ 1 in PrimRec by A2, 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 that
A4: 1 <= i and
A5: i <= n ; :: thesis: n proj i in PrimRec

now

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

end;

hence n proj i in PrimRec by A2, 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 that
A6: f in PrimRec and
A7: arity f = len F and
A8: rng F c= PrimRec ; :: thesis: f * <:F:> in PrimRec

now

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

end;

hence f * <:F:> in PrimRec by A2, 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
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

let Y be set ; :: thesis: ( Y in { R where R is Subset of : R is primitive-recursively_closed } implies g in Y )
assume A17: Y in { R where R is Subset of : R is primitive-recursively_closed } ; :: thesis: g in Y
then consider R being Subset of 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, Def17;
f1 in R by A15, A17, A18, SETFAM_1:def 1;
hence g in Y by A14, A18, A21, A20, Def16; :: thesis: verum

end;

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

end;

end;