set NN = Funcs (NAT,NAT);
defpred S₁[ Nat, object , object ] means for h being Function of (Segm ($1 + 1)),(Funcs (NAT,NAT)) st h = $2 holds
( $3 is Function of (Segm (($1 + 1) + 1)),(Funcs (NAT,NAT)) & ( for t being Function of (Segm (($1 + 1) + 1)),(Funcs (NAT,NAT)) st t = $3 holds
( t | (Segm ($1 + 1)) = h & ( for ti being Function of NAT,NAT st ti = t . ($1 + 1) holds
( ti . 0 = (h . $1) . 1 & ( for n being Nat holds ti . (n + 1) = (h . $1) . (ti . n) ) ) ) ) ) );
defpred S₂[ object , object ] means for i being Nat st i = $1 holds
( $2 is Function of (Funcs ((Segm (i + 1)),(Funcs (NAT,NAT)))),(Funcs ((Segm ((i + 1) + 1)),(Funcs (NAT,NAT)))) & ( for g being Function of (Funcs ((Segm (i + 1)),(Funcs (NAT,NAT)))),(Funcs ((Segm ((i + 1) + 1)),(Funcs (NAT,NAT)))) st g = $2 holds
for h being Function of (Segm (i + 1)),(Funcs (NAT,NAT)) holds S₁[i,h,g . h] ) );
A1: for i being object st i in NAT holds
ex H being object st S₂[i,H]

let x be object ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider i = x as Element of NAT ;
defpred S₃[ object , object ] means S₁[i,$1,$2];
A2: for x being object st x in Funcs ((Segm (i + 1)),(Funcs (NAT,NAT))) holds
ex y being object st
( y in Funcs ((Segm ((i + 1) + 1)),(Funcs (NAT,NAT))) & S₃[x,y] )

let x be object ; :: thesis:
assume A3: x in Funcs ((Segm (i + 1)),(Funcs (NAT,NAT))) ; :: thesis:
reconsider h = x as Function of (Segm (i + 1)),(Funcs (NAT,NAT)) by A3, FUNCT_2:66;
defpred S₄[ object , object ] means for n being Nat st n = $1 holds
( ( n <= i implies $2 = h . $1 ) & ( n = i + 1 implies ( $2 is Function of NAT,NAT & ( for ti being Function of NAT,NAT st ti = $2 holds
( ti . 0 = (h . i) . 1 & ( for n being Nat holds ti . (n + 1) = (h . i) . (ti . n) ) ) ) ) ) );
A4: for z being object st z in Segm ((i + 1) + 1) holds
ex t being object st
( t in Funcs (NAT,NAT) & S₄[z,t] )

proof

let c be object ; :: thesis:
assume A5: c in Segm ((i + 1) + 1) ; :: thesis:
reconsider z = c as Nat by A5;
z < (i + 1) + 1 by A5, NAT_1:44;
then z <= i + 1 by NAT_1:13;

per cases by XXREAL_0:1;

suppose A6: z < i + 1 ; :: thesis:

take hz = h . z; :: thesis:
( z in Segm (i + 1) & Segm (i + 1) = dom h ) by A6, FUNCT_2:def 1, NAT_1:44;
then ( h . z in rng h & rng h c= Funcs (NAT,NAT) ) by FUNCT_1:def 3;
hence ( hz in Funcs (NAT,NAT) & S₄[c,hz] ) by A6; :: thesis:

end;

suppose A7: z = i + 1 ; :: thesis:

deffunc H₁( object , object ) -> set = (h . i) . $2;
consider t being Function such that
A8: ( dom t = NAT & t . 0 = (h . i) . 1 ) and
A9: for n being Nat holds t . (n + 1) = H₁(n,t . n) from NAT_1:sch 11();
take t ; :: thesis:
rng t c= NAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A10: y in rng t ; :: thesis:
consider x being object such that
A11: ( x in dom t & t . x = y ) by A10, FUNCT_1:def 3;
reconsider x = x as Nat by A11, A8;
i < i + 1 by NAT_1:13;
then ( i in Segm (i + 1) & Segm (i + 1) = dom h ) by NAT_1:44, FUNCT_2:def 1;
then ( h . i in rng h & rng h c= Funcs (NAT,NAT) ) by FUNCT_1:def 3;
then reconsider hi = h . i as Function of NAT,NAT by FUNCT_2:66;
defpred S₅[ Nat] means t . $1 in NAT ;
A12: ( dom hi = NAT & rng hi c= NAT ) by FUNCT_2:def 1;
hi . 1 in rng hi by A12, FUNCT_1:def 3;
then A13: S₅[ 0 ] by A8;
A14: for j being Nat st S₅[j] holds
S₅[j + 1]

proof

let j be Nat; :: thesis:
assume S₅[j] ; :: thesis:
then ( t . (j + 1) = hi . (t . j) & hi . (t . j) in rng hi ) by A12, A9, FUNCT_1:def 3;
hence S₅[j + 1] ; :: thesis:

end;

for j being Nat holds S₅[j] from NAT_1:sch 2(A13, A14);
then t . x in NAT ;
hence y in NAT by A11; :: thesis:

end;

then t is Function of NAT,NAT by A8, FUNCT_2:2;
hence ( t in Funcs (NAT,NAT) & S₄[c,t] ) by A7, NAT_1:13, A8, A9, FUNCT_2:9; :: thesis:

end;

consider P being Function such that
A15: ( dom P = Segm ((i + 1) + 1) & rng P c= Funcs (NAT,NAT) & ( for z being object st z in Segm ((i + 1) + 1) holds
S₄[z,P . z] ) ) from FUNCT_1:sch 6(A4);
take P ; :: thesis:
thus A16: P in Funcs ((Segm ((i + 1) + 1)),(Funcs (NAT,NAT))) by A15, FUNCT_2:def 2; :: thesis:
thus S₁[i,x,P] :: thesis:

proof

let h1 be Function of (Segm (i + 1)),(Funcs (NAT,NAT)); :: thesis:
assume A17: h1 = x ; :: thesis:
thus P is Function of (Segm ((i + 1) + 1)),(Funcs (NAT,NAT)) by A16, FUNCT_2:66; :: thesis:
let t be Function of (Segm ((i + 1) + 1)),(Funcs (NAT,NAT)); :: thesis:
assume A18: t = P ; :: thesis:
A19: dom h1 = Segm (i + 1) by FUNCT_2:def 1;
A20: i + 1 < (i + 1) + 1 by NAT_1:13;
then A21: ( Segm (i + 1) c= Segm ((i + 1) + 1) & Segm ((i + 1) + 1) = dom t ) by NAT_1:39, FUNCT_2:def 1;
then A22: dom (t | (Segm (i + 1))) = Segm (i + 1) by RELAT_1:62;
for z being object st z in Segm (i + 1) holds
(t | (Segm (i + 1))) . z = h1 . z

proof

let z be object ; :: thesis:
assume A23: z in Segm (i + 1) ; :: thesis:
reconsider z = z as Nat by A23;
z < i + 1 by A23, NAT_1:44;
then z <= i by NAT_1:13;
then P . z = h . z by A15, A23, A21;
hence (t | (Segm (i + 1))) . z = h1 . z by A17, A18, A23, FUNCT_1:49; :: thesis:

end;

hence t | (Segm (i + 1)) = h1 by A19, A22, FUNCT_1:2; :: thesis:
let ti be Function of NAT,NAT; :: thesis:
assume A24: ti = t . (i + 1) ; :: thesis:
i + 1 in Segm ((i + 1) + 1) by A20, NAT_1:44;
hence ( ti . 0 = (h1 . i) . 1 & ( for n being Nat holds ti . (n + 1) = (h1 . i) . (ti . n) ) ) by A24, A17, A18, A15; :: thesis:

end;

consider H being Function such that
A25: ( dom H = Funcs ((Segm (i + 1)),(Funcs (NAT,NAT))) & rng H c= Funcs ((Segm ((i + 1) + 1)),(Funcs (NAT,NAT))) & ( for x being object st x in Funcs ((Segm (i + 1)),(Funcs (NAT,NAT))) holds
S₃[x,H . x] ) ) from FUNCT_1:sch 6(A2);
take H ; :: thesis:
let j be Nat; :: thesis:
assume A26: j = x ; :: thesis:
thus H is Function of (Funcs ((Segm (j + 1)),(Funcs (NAT,NAT)))),(Funcs ((Segm ((j + 1) + 1)),(Funcs (NAT,NAT)))) by A26, A25, FUNCT_2:2; :: thesis:
let g be Function of (Funcs ((Segm (j + 1)),(Funcs (NAT,NAT)))),(Funcs ((Segm ((j + 1) + 1)),(Funcs (NAT,NAT)))); :: thesis:
assume A27: g = H ; :: thesis:
let h be Function of (Segm (j + 1)),(Funcs (NAT,NAT)); :: thesis:
h in Funcs ((Segm (i + 1)),(Funcs (NAT,NAT))) by A26, FUNCT_2:8;
hence S₁[j,h,g . h] by A25, A27, A26; :: thesis:

end;

consider GG being Function such that
A28: ( dom GG = NAT & ( for i being object st i in NAT holds
S₂[i,GG . i] ) ) from CLASSES1:sch 1(A1);
for x being object st x in dom GG holds
GG . x is Function by A28;
then reconsider GG = GG as Function-yielding Function by FUNCOP_1:def 6;
deffunc H₁( object , object ) -> set = (GG . $1) . $2;
deffunc H₂( Element of NAT ) -> Element of omega = $1 + 1;
consider a0 being Function of NAT,NAT such that
A29: for x being Element of NAT holds a0 . x = H₂(x) from FUNCT_2:sch 4();
set f0 = (Segm 1) --> a0;
a0 in Funcs (NAT,NAT) by FUNCT_2:8;
then A30: {a0} c= Funcs (NAT,NAT) by ZFMISC_1:31;
A31: ( rng ((Segm 1) --> a0) = {a0} & dom ((Segm 1) --> a0) = Segm 1 ) by FUNCOP_1:8;
consider Ack being Function such that
A32: ( dom Ack = NAT & Ack . 0 = (Segm 1) --> a0 ) and
A33: for n being Nat holds Ack . (n + 1) = H₁(n,Ack . n) from NAT_1:sch 11();
defpred S₃[ Nat] means Ack . $1 in Funcs ((Segm ($1 + 1)),(Funcs (NAT,NAT)));
A34: S₃[ 0 ] by A32, A31, A30, FUNCT_2:def 2;
A35: for j being Nat st S₃[j] holds
S₃[j + 1]

proof

let j be Nat; :: thesis:
assume A36: S₃[j] ; :: thesis:
j in NAT by ORDINAL1:def 12;
then reconsider GGj = GG . j as Function of (Funcs ((Segm (j + 1)),(Funcs (NAT,NAT)))),(Funcs ((Segm ((j + 1) + 1)),(Funcs (NAT,NAT)))) by A28;
A37: Ack . (j + 1) = GGj . (Ack . j) by A33;
Funcs ((Segm (j + 1)),(Funcs (NAT,NAT))) = dom GGj by FUNCT_2:def 1;
then ( GGj . (Ack . j) in rng GGj & rng GGj c= Funcs ((Segm ((j + 1) + 1)),(Funcs (NAT,NAT))) ) by A36, FUNCT_1:def 3;
hence S₃[j + 1] by A37; :: thesis:

end;

A38: for j being Nat holds S₃[j] from NAT_1:sch 2(A34, A35);
for x being object st x in dom Ack holds
Ack . x is Function

proof

let x be object ; :: thesis:
assume x in dom Ack ; :: thesis:
then reconsider x = x as Nat by A32;
Ack . x in Funcs ((Segm (x + 1)),(Funcs (NAT,NAT))) by A38;
hence Ack . x is Function ; :: thesis:

end;

then reconsider Ack = Ack as Function-yielding Function by FUNCOP_1:def 6;
defpred S₄[ object , object , object ] means for A being Function of NAT,NAT st A = (Ack . $1) . $1 holds
$3 = A . $2;
A39: for x, y being object st x in NAT & y in NAT holds
ex z being object st
( z in NAT & S₄[x,y,z] )

proof

let x, y be object ; :: thesis:
assume A40: ( x in NAT & y in NAT ) ; :: thesis:
reconsider x = x as Nat by A40;
Ack . x in Funcs ((Segm (x + 1)),(Funcs (NAT,NAT))) by A38;
then reconsider Ackx = Ack . x as Function of (Segm (x + 1)),(Funcs (NAT,NAT)) by FUNCT_2:66;
x < x + 1 by NAT_1:13;
then ( x in Segm (x + 1) & Segm (x + 1) = dom Ackx ) by NAT_1:44, FUNCT_2:def 1;
then ( Ackx . x in rng Ackx & rng Ackx c= Funcs (NAT,NAT) ) by FUNCT_1:def 3;
then reconsider Ackxx = Ackx . x as Function of NAT,NAT by FUNCT_2:66;
take z = Ackxx . y; :: thesis:
dom Ackxx = NAT by FUNCT_2:def 1;
then ( z in rng Ackxx & rng Ackxx c= NAT ) by A40, FUNCT_1:def 3;
hence ( z in NAT & S₄[x,y,z] ) ; :: thesis:

end;

consider IT being BinOp of NAT such that
A41: for x, y being object st x in NAT & y in NAT holds
S₄[x,y,IT . (x,y)] from BINOP_1:sch 1(A39);
take IT ; :: thesis:
let m, n be Nat; :: thesis:
A42: n in NAT by ORDINAL1:def 12;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
((Segm 1) --> a0) . 0 = a0 by NAT_1:44, FUNCOP_1:7;
then IT . (0,n) = a0 . n by A32, A41, A42;
hence IT . (0,n) = n + 1 by A42, A29; :: thesis:
( m > 0 implies ( IT . (m,0) = IT . ((m - 1),1) & ( n > 0 implies IT . (m,n) = IT . ((m - 1),(IT . (m,(n - 1)))) ) ) )

proof

assume m > 0 ; :: thesis:
then reconsider m1 = m - 1 as Element of NAT by NAT_1:20;
Ack . m in Funcs ((Segm (m + 1)),(Funcs (NAT,NAT))) by A38;
then reconsider Ackm = Ack . m as Function of (Segm (m + 1)),(Funcs (NAT,NAT)) by FUNCT_2:66;
m < m + 1 by NAT_1:13;
then ( m in Segm (m + 1) & Segm (m + 1) = dom Ackm ) by NAT_1:44, FUNCT_2:def 1;
then ( Ackm . m in rng Ackm & rng Ackm c= Funcs (NAT,NAT) ) by FUNCT_1:def 3;
then reconsider Ackmm = Ackm . m as Function of NAT,NAT by FUNCT_2:66;
Ack . m1 in Funcs ((Segm (m1 + 1)),(Funcs (NAT,NAT))) by A38;
then reconsider Ackm1 = Ack . m1 as Function of (Segm (m1 + 1)),(Funcs (NAT,NAT)) by FUNCT_2:66;
m1 < m1 + 1 by NAT_1:13;
then ( m1 in Segm (m1 + 1) & Segm (m1 + 1) = dom Ackm1 ) by NAT_1:44, FUNCT_2:def 1;
then ( Ackm1 . m1 in rng Ackm1 & rng Ackm1 c= Funcs (NAT,NAT) ) by FUNCT_1:def 3;
then reconsider Ackm1m1 = Ackm1 . m1 as Function of NAT,NAT by FUNCT_2:66;
reconsider GGm = GG . m as Function of (Funcs ((Segm (m + 1)),(Funcs (NAT,NAT)))),(Funcs ((Segm ((m + 1) + 1)),(Funcs (NAT,NAT)))) by A28;
reconsider GGmA = GGm . Ackm as Function of (Segm ((m + 1) + 1)),(Funcs (NAT,NAT)) by A28;
m + 1 < (m + 1) + 1 by NAT_1:13;
then ( m + 1 in Segm ((m + 1) + 1) & Segm ((m + 1) + 1) = dom GGmA ) by NAT_1:44, FUNCT_2:def 1;
then ( GGmA . (m + 1) in rng GGmA & rng GGmA c= Funcs (NAT,NAT) ) by FUNCT_1:def 3;
then reconsider GGmAm = GGmA . (m + 1) as Function of NAT,NAT by FUNCT_2:66;
reconsider GGm1 = GG . m1 as Function of (Funcs ((Segm (m1 + 1)),(Funcs (NAT,NAT)))),(Funcs ((Segm ((m1 + 1) + 1)),(Funcs (NAT,NAT)))) by A28;
reconsider GGm1A = GGm1 . Ackm1 as Function of (Segm ((m1 + 1) + 1)),(Funcs (NAT,NAT)) by A28;
m1 + 1 < (m1 + 1) + 1 by NAT_1:13;
then ( m1 + 1 in Segm ((m1 + 1) + 1) & Segm ((m1 + 1) + 1) = dom GGm1A ) by NAT_1:44, FUNCT_2:def 1;
then ( GGm1A . (m1 + 1) in rng GGm1A & rng GGm1A c= Funcs (NAT,NAT) ) by FUNCT_1:def 3;
then reconsider GGm1Am = GGm1A . (m1 + 1) as Function of NAT,NAT by FUNCT_2:66;
A43: Ackmm = GGm1A . m by A33;
then A44: Ackmm . 0 = (Ackm1 . m1) . 1 by A28;
IT . (m1,1) = Ackm1m1 . 1 by A41;
hence IT . (m,0) = IT . ((m - 1),1) by A44, A41; :: thesis:
assume n > 0 ; :: thesis:
then reconsider n1 = n - 1 as Element of NAT by NAT_1:20;
IT . (m,n) = Ackmm . (n1 + 1) by A41;
then A45: IT . (m,n) = (Ackm1 . m1) . (GGm1Am . n1) by A28, A43;
IT . (m1,(IT . (m,n1))) = Ackm1m1 . (IT . (m,n1)) by A41;
hence IT . (m,n) = IT . ((m - 1),(IT . (m,(n - 1)))) by A45, A43, A41; :: thesis:

end;

hence ( ( m > 0 implies IT . (m,0) = IT . ((m - 1),1) ) & ( m > 0 & n > 0 implies IT . (m,n) = IT . ((m - 1),(IT . (m,(n - 1)))) ) ) ; :: thesis: