set D = 1 -aryPrimRecFuncs ;
reconsider d = 1 succ 1 as Element of 1 -aryPrimRecFuncs by Th34;
defpred S₁[ Nat, set , set ] means ( ( $1 = 0 implies $3 = primrec ((0 const H₁( 0 ,1)),((1 succ 1) * <:<*(2 proj 2)*>:>),1) ) & ( $1 <> 0 implies ex g being primitive-recursive 1 -ary Function st
( $2 = g & $3 = primrec ((0 const H₁($1,1)),(g * <:<*(2 proj 2)*>:>),1) ) ) );
A1: for n being Nat
for x being Element of 1 -aryPrimRecFuncs ex y being Element of 1 -aryPrimRecFuncs st S₁[n,x,y]

proof

let n be Nat; :: thesis: for x being Element of 1 -aryPrimRecFuncs ex y being Element of 1 -aryPrimRecFuncs st S₁[n,x,y]
let x be Element of 1 -aryPrimRecFuncs ; :: thesis: ex y being Element of 1 -aryPrimRecFuncs st S₁[n,x,y]

per cases ( n = 0 or ex a being Nat st n = a + 1 ) by NAT_1:6;

suppose A2: n = 0 ; :: thesis: ex y being Element of 1 -aryPrimRecFuncs st S₁[n,x,y]

set y = primrec ((0 const H₁( 0 ,1)),((1 succ 1) * <:<*(2 proj 2)*>:>),1);
primrec ((0 const H₁( 0 ,1)),((1 succ 1) * <:<*(2 proj 2)*>:>),1) in 1 -aryPrimRecFuncs ;
then reconsider y = primrec ((0 const H₁( 0 ,1)),((1 succ 1) * <:<*(2 proj 2)*>:>),1) as Element of 1 -aryPrimRecFuncs ;
take y ; :: thesis: S₁[n,x,y]
thus S₁[n,x,y] by A2; :: thesis: verum

end;

suppose ex a being Nat st n = a + 1 ; :: thesis: ex y being Element of 1 -aryPrimRecFuncs st S₁[n,x,y]

then consider a being Nat such that
A3: n = a + 1 ;
x in 1 -aryPrimRecFuncs ;
then consider g being Element of HFuncs NAT such that
A4: x = g and
A5: ( g is 1 -ary & g is primitive-recursive ) ;
reconsider g = g as primitive-recursive 1 -ary Function by A5;
set y = primrec ((0 const H₁(n,1)),(g * <:<*(2 proj 2)*>:>),1);
primrec ((0 const H₁(n,1)),(g * <:<*(2 proj 2)*>:>),1) in 1 -aryPrimRecFuncs ;
then reconsider y = primrec ((0 const H₁(n,1)),(g * <:<*(2 proj 2)*>:>),1) as Element of 1 -aryPrimRecFuncs ;
take y ; :: thesis: S₁[n,x,y]
thus S₁[n,x,y] by A3, A4; :: thesis: verum

end;

end;

end;

consider f being sequence of (1 -aryPrimRecFuncs) such that
A6: f . 0 = d and
A7: for n being Nat holds S₁[n,f . n,f . (n + 1)] from RECDEF_1:sch 2(A1);
reconsider f = f as Function-yielding ManySortedSet of NAT ;
f is homogeneous

proof

let n be Nat; :: according to ACKERMAN:def 6 :: thesis: f . n is homogeneous

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: f . n is homogeneous

hence f . n is homogeneous by A6; :: thesis: verum

end;

suppose A8: n <> 0 ; :: thesis: f . n is homogeneous

S₁[n,f . n,f . (n + 1)] by A7;
hence f . n is homogeneous by A8; :: thesis: verum

end;

end;

end;

then reconsider f = f as Function-yielding homogeneous ManySortedSet of NAT ;
A9: f is 1 -ary

proof

let n be Nat; :: according to ACKERMAN:def 11 :: thesis: f . n is 1 -ary

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: f . n is 1 -ary

hence f . n is 1 -ary by A6; :: thesis: verum

end;

suppose A10: n <> 0 ; :: thesis: f . n is 1 -ary

S₁[n,f . n,f . (n + 1)] by A7;
hence f . n is 1 -ary by A10; :: thesis: verum

end;

end;

end;

A11: f is primitive-recursive

proof

let n be Nat; :: according to ACKERMAN:def 8 :: thesis: f . n is primitive-recursive

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: f . n is primitive-recursive

hence f . n is primitive-recursive by A6; :: thesis: verum

end;

suppose A12: n <> 0 ; :: thesis: f . n is primitive-recursive

S₁[n,f . n,f . (n + 1)] by A7;
hence f . n is primitive-recursive by A12; :: thesis: verum

end;

end;

end;

A13: f is to-naturals

proof

let n be Nat; :: according to ACKERMAN:def 7 :: thesis: f . n is to-naturals

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: f . n is to-naturals

hence f . n is to-naturals by A6; :: thesis: verum

end;

suppose A14: n <> 0 ; :: thesis: f . n is to-naturals

S₁[n,f . n,f . (n + 1)] by A7;
hence f . n is to-naturals by A14; :: thesis: verum

end;

end;

end;

f is NAT * -defined by A11;
then reconsider f = f as Function-yielding primitive-recursive satisfying_primrec_conditions 1 -ary ManySortedSet of NAT by A9, A11, A13;
take f ; :: thesis: ( f . 0 = 1 succ 1 & ( for m being Nat holds f . (m + 1) = primrec ((0 const (Ackermann (m,1))),((f . m) * <:<*(2 proj 2)*>:>),1) ) )
thus f . 0 = 1 succ 1 by A6; :: thesis: for m being Nat holds f . (m + 1) = primrec ((0 const (Ackermann (m,1))),((f . m) * <:<*(2 proj 2)*>:>),1)
let n be Nat; :: thesis: f . (n + 1) = primrec ((0 const (Ackermann (n,1))),((f . n) * <:<*(2 proj 2)*>:>),1)

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: f . (n + 1) = primrec ((0 const (Ackermann (n,1))),((f . n) * <:<*(2 proj 2)*>:>),1)

hence f . (n + 1) = primrec ((0 const (Ackermann (n,1))),((f . n) * <:<*(2 proj 2)*>:>),1) by A6, A7; :: thesis: verum

end;

suppose A15: n <> 0 ; :: thesis: f . (n + 1) = primrec ((0 const (Ackermann (n,1))),((f . n) * <:<*(2 proj 2)*>:>),1)

S₁[n,f . n,f . (n + 1)] by A7;
hence f . (n + 1) = primrec ((0 const (Ackermann (n,1))),((f . n) * <:<*(2 proj 2)*>:>),1) by A15; :: thesis: verum

end;

end;