let n, c be Element of NAT ; :: thesis:
let P be non empty primitive-recursively_closed Subset of (HFuncs NAT ); :: thesis:
A1: P is composition_closed by Def17;
defpred S₂[ Element of NAT ] means 0 const $1 in P;
A2: S₂[ 0 ] by Def17;
A3: for i being Element of NAT st S₂[i] holds
S₂[i + 1]

proof

let i be Element of NAT ; :: thesis:
set F = <*(0 const i)*>;
reconsider 0consti = 0 const i as Element of HFuncs NAT by Th31;
<*0consti*> is FinSequence of HFuncs NAT ;
then reconsider F = <*(0 const i)*> as with_the_same_arity FinSequence of HFuncs NAT ;
assume 0 const i in P ; :: thesis:
then A4: ( {(0 const i)} c= P & rng F = {(0 const i)} ) by FINSEQ_1:56, ZFMISC_1:37;
A5: 1 succ 1 in P by Def17;
A6: arity (1 succ 1) = 1 by Th38
.= len F by FINSEQ_1:56 ;
reconsider 1succ1 = 1 succ 1 as quasi_total Element of HFuncs NAT by Th32;

now

let h be Element of HFuncs NAT ; :: thesis:
assume h in rng F ; :: thesis:
then h = 0 const i by A4, TARSKI:def 1;
hence h is quasi_total by Th32; :: thesis:

end;

then reconsider g = 1succ1 * <:F:> as quasi_total Element of HFuncs NAT by A6, Th50;
A7: ( arity (0 const (i + 1)) = 0 & arity (0 const i) = 0 ) by Th35;
A8: <*> NAT is Element of 0 -tuples_on NAT by FINSEQ_2:114;
then A9: ( (0 const (i + 1)) . {} = i + 1 & (0 const i) . {} = i ) by FUNCOP_1:13;
A10: dom <:<*(0 const i)*>:> = dom (0 const i) by FUNCT_6:61;
A11: dom (0 const i) = 0 -tuples_on NAT by A7, Th26;
then A12: <:<*(0 const i)*>:> . {} = <*i*> by A8, A9, FUNCT_6:61;
dom (1 succ 1) = 1 -tuples_on NAT by Def10;
then A13: {} in dom g by A8, A10, A11, A12, FUNCT_1:21;
0 const i in rng F by A4, TARSKI:def 1;
then arity F = 0 by A7, Def7;
then A14: arity g = 0 by A13, Th48, RELAT_1:60;
dom (0 const i) = 0 -tuples_on NAT by A7, Th26;
then ( g . {} = (1 succ 1) . (<:F:> . {} ) & <:F:> . {} = <*i*> & <*i*> is Element of 1 -tuples_on NAT ) by A8, A9, A10, FUNCT_1:23, FUNCT_6:61;
then g . {} = (<*i*> /. 1) + 1 by Def10
.= i + 1 by FINSEQ_4:25 ;
then 0 const (i + 1) = (1 succ 1) * <:<*(0 const i)*>:> by A7, A9, A13, A14, Th52, RELAT_1:60;
hence 0 const (i + 1) in P by A1, A4, A5, A6, Def15; :: thesis:

end;

A15: P is primitive-recursion_closed by Def17;
A16: for i being Element of NAT holds S₂[i] from NAT_1:sch 1(A2, A3);
defpred S₃[ Element of NAT ] means for c being Element of NAT holds $1 const c in P;
A17: S₃[ 0 ] by A16;

A18: now

let n be Element of NAT ; :: thesis:
assume A19: S₃[n] ; :: thesis:
thus S₃[n + 1] :: thesis:

proof

let i be Element of NAT ; :: thesis:
set g = (n + 1) const i;
set f1 = n const i;
set j = n + 1;
set f2 = (n + 2) proj (n + 2);
A20: arity ((n + 1) const i) = n + 1 by Th35;
A21: dom ((n + 1) const i) = (n + 1) -tuples_on NAT by FUNCOP_1:19;
A22: arity (n const i) = n by Th35;
A23: dom (n const i) = n -tuples_on NAT by FUNCOP_1:19;
A24: dom ((n + 2) proj (n + 2)) = (n + 2) -tuples_on NAT by Th40;
A25: arity ((n + 2) proj (n + 2)) = n + 2 by Th41;
A26: n + (1 + 1) = (n + 1) + 1 ;
A27: (n + 1) const i is_primitive-recursively_expressed_by n const i,(n + 2) proj (n + 2),n + 1

proof

take m = arity ((n + 1) const i); :: according to COMPUT_1:def 12 :: thesis:
thus dom ((n + 1) const i) c= m -tuples_on NAT by Th24; :: thesis:
thus ( n + 1 >= 1 & n + 1 <= m ) by Th35, NAT_1:11; :: thesis:
thus ( (arity (n const i)) + 1 = m & m + 1 = arity ((n + 2) proj (n + 2)) ) by A22, A25, A26, Th35; :: thesis:
let p be FinSequence of NAT ; :: thesis:
assume len p = m ; :: thesis:
then A28: ( p is Element of (n + 1) -tuples_on NAT & n + 1 >= 1 ) by A20, FINSEQ_2:110, NAT_1:11;
then A29: (n const i) . (Del p,(n + 1)) = i by Th12, FUNCOP_1:13;
thus ( p +* (n + 1),0 in dom ((n + 1) const i) implies Del p,(n + 1) in dom (n const i) ) by A23, A28, Th12; :: thesis:
thus ( Del p,(n + 1) in dom (n const i) implies p +* (n + 1),0 in dom ((n + 1) const i) ) by A21, A28, Lm7; :: thesis:
thus ( p +* (n + 1),0 in dom ((n + 1) const i) implies ((n + 1) const i) . (p +* (n + 1),0 ) = (n const i) . (Del p,(n + 1)) ) by A28, A29, Lm7, FUNCOP_1:13; :: thesis:
let m be Element of NAT ; :: thesis:
A30: p +* (n + 1),m in (n + 1) -tuples_on NAT by A28, Lm7;
then len (p +* (n + 1),m) = n + 1 by FINSEQ_2:109;
then A31: ((p +* (n + 1),m) ^ <*i*>) . ((n + 1) + 1) = i by FINSEQ_1:59;
A32: (p +* (n + 1),m) ^ <*i*> is Element of (n + 2) -tuples_on NAT by A26, A30, FINSEQ_2:127;

hereby :: thesis:

assume p +* (n + 1),(m + 1) in dom ((n + 1) const i) ; :: thesis:
thus p +* (n + 1),m in dom ((n + 1) const i) by A21, A28, Lm7; :: thesis:
((n + 1) const i) . (p +* (n + 1),m) = i by A28, Lm7, FUNCOP_1:13;
hence (p +* (n + 1),m) ^ <*(((n + 1) const i) . (p +* (n + 1),m))*> in dom ((n + 2) proj (n + 2)) by A24, A32; :: thesis:

end;

thus ( p +* (n + 1),m in dom ((n + 1) const i) & (p +* (n + 1),m) ^ <*(((n + 1) const i) . (p +* (n + 1),m))*> in dom ((n + 2) proj (n + 2)) implies p +* (n + 1),(m + 1) in dom ((n + 1) const i) ) by A21, A28, Lm7; :: thesis:

end;

assume p +* (n + 1),(m + 1) in dom ((n + 1) const i) ; :: thesis:
thus ((n + 1) const i) . (p +* (n + 1),(m + 1)) = i by A28, Lm7, FUNCOP_1:13
.= ((n + 2) proj (n + 2)) . ((p +* (n + 1),m) ^ <*i*>) by A31, A32, Th42
.= ((n + 2) proj (n + 2)) . ((p +* (n + 1),m) ^ <*(((n + 1) const i) . (p +* (n + 1),m))*>) by A28, Lm7, FUNCOP_1:13 ; :: thesis:

end;

A33: ( n const i is Element of HFuncs NAT & (n + 2) proj (n + 2) is Element of HFuncs NAT & (n + 1) const i is Element of HFuncs NAT ) by Th31;
1 <= n + 2 by A26, NAT_1:11;
then ( n const i in P & (n + 2) proj (n + 2) in P ) by A19, Def17;
hence (n + 1) const i in P by A15, A27, A33, Def16; :: thesis:

end;

for n being Element of NAT holds S₃[n] from NAT_1:sch 1(A17, A18);
hence n const c in P ; :: thesis: