defpred S₁[ set , set , set ] means ex O2 being Ordinal st
( O2 = $3 & ( for X being set
for n being Element of NAT st X c= Rank (the_rank_of $2) holds
ex Y being set st
( Y c= Rank O2 & P₁[n,X,Y] ) ) & ( for O being Ordinal st ( for X being set
for n being Element of NAT st X c= Rank (the_rank_of $2) holds
ex Y being set st
( Y c= Rank O & P₁[n,X,Y] ) ) holds
O2 c= O ) );
A2: for n being Element of NAT
for x being set ex y being set st S₁[n,x,y]

defpred S₂[ set , set ] means for m being Element of NAT ex y being set st
( $2 is Ordinal & y c= Rank (the_rank_of $2) & P₁[m,$1,y] );
let n be Element of NAT ; :: thesis:
let x be set ; :: thesis:
defpred S₃[ Ordinal] means for X being set
for n being Element of NAT st X c= Rank (the_rank_of x) holds
ex Y being set st
( Y c= Rank $1 & P₁[n,X,Y] );
A3: for x9 being set st x9 in bool (Rank (the_rank_of x)) holds
ex o being set st S₂[x9,o]

let x9 be set ; :: thesis:
assume x9 in bool (Rank (the_rank_of x)) ; :: thesis:
defpred S₄[ set , set ] means ex y being set st
( $2 is Ordinal & y c= Rank (the_rank_of $2) & P₁[$1,x9,y] );
A4: for e being set st e in NAT holds
ex u being set st S₄[e,u]

let i be set ; :: thesis:
assume i in NAT ; :: thesis:
then reconsider i9 = i as Element of NAT ;
thus ex o, y being set st
( o is Ordinal & y c= Rank (the_rank_of o) & P₁[i,x9,y] ) :: thesis:

consider y being set such that
A5: P₁[i9,x9,y] by A1;
take o = the_rank_of y; :: thesis:
take y ; :: thesis:
thus o is Ordinal ; :: thesis:
the_rank_of (the_rank_of y) = the_rank_of y by CLASSES1:81;
hence y c= Rank (the_rank_of o) by CLASSES1:73; :: thesis:
thus P₁[i,x9,y] by A5; :: thesis:

end;

end;

consider h being Function such that
A6: dom h = NAT and
A7: for i being set st i in NAT holds
S₄[i,h . i] from CLASSES1:sch 1(A4);
take o = sup (rng h); :: thesis:
thus for m being Element of NAT ex y being set st
( o is Ordinal & y c= Rank (the_rank_of o) & P₁[m,x9,y] ) :: thesis:

let m be Element of NAT ; :: thesis:
consider y being set such that
A8: h . m is Ordinal and
A9: y c= Rank (the_rank_of (h . m)) and
A10: P₁[m,x9,y] by A7;
reconsider O = h . m as Ordinal by A8;
h . m in rng h by A6, FUNCT_1:def 5;
then h . m in sup (rng h) by A8, ORDINAL2:27;
then h . m c= o by ORDINAL1:def 2;
then A11: Rank O c= Rank o by CLASSES1:43;
take y ; :: thesis:
thus o is Ordinal ; :: thesis:
y c= Rank O by A9, CLASSES1:81;
then y c= Rank o by A11, XBOOLE_1:1;
hence y c= Rank (the_rank_of o) by CLASSES1:81; :: thesis:
thus P₁[m,x9,y] by A10; :: thesis:

end;

end;

consider f being Function such that
A12: dom f = bool (Rank (the_rank_of x)) and
A13: for x9 being set st x9 in bool (Rank (the_rank_of x)) holds
S₂[x9,f . x9] from CLASSES1:sch 1(A3);
A14: ex O being Ordinal st S₃[O]

take O2 = sup (rng f); :: thesis:
thus for X being set
for m being Element of NAT st X c= Rank (the_rank_of x) holds
ex Y being set st
( Y c= Rank O2 & P₁[m,X,Y] ) :: thesis:

let X be set ; :: thesis:
let m be Element of NAT ; :: thesis:
assume A15: X c= Rank (the_rank_of x) ; :: thesis:
then consider Y being set such that
A16: f . X is Ordinal and
A17: Y c= Rank (the_rank_of (f . X)) and
A18: P₁[m,X,Y] by A13;
reconsider O = f . X as Ordinal by A16;
f . X in rng f by A12, A15, FUNCT_1:def 5;
then f . X in sup (rng f) by A16, ORDINAL2:27;
then f . X c= O2 by ORDINAL1:def 2;
then A19: Rank O c= Rank O2 by CLASSES1:43;
take Y ; :: thesis:
the_rank_of O = O by CLASSES1:81;
hence Y c= Rank O2 by A17, A19, XBOOLE_1:1; :: thesis:
thus P₁[m,X,Y] by A18; :: thesis:

end;

end;

consider O2 being Ordinal such that
A20: ( S₃[O2] & ( for O being Ordinal st S₃[O] holds
O2 c= O ) ) from ORDINAL1:sch 1(A14);
take O2 ; :: thesis:
thus S₁[n,x,O2] by A20; :: thesis:

end;

A21: for n being Element of NAT
for x, y1, y2 being set st S₁[n,x,y1] & S₁[n,x,y2] holds
y1 = y2

let n be Element of NAT ; :: thesis:
let x, y1, y2 be set ; :: thesis:
assume that
A22: S₁[n,x,y1] and
A23: S₁[n,x,y2] ; :: thesis:
consider O2 being Ordinal such that
A24: O2 = y2 and
A25: ( ( for X being set
for n being Element of NAT st X c= Rank (the_rank_of x) holds
ex Y being set st
( Y c= Rank O2 & P₁[n,X,Y] ) ) & ( for O being Ordinal st ( for X being set
for n being Element of NAT st X c= Rank (the_rank_of x) holds
ex Y being set st
( Y c= Rank O & P₁[n,X,Y] ) ) holds
O2 c= O ) ) by A23;
consider O1 being Ordinal such that
A26: O1 = y1 and
A27: ( ( for X being set
for n being Element of NAT st X c= Rank (the_rank_of x) holds
ex Y being set st
( Y c= Rank O1 & P₁[n,X,Y] ) ) & ( for O being Ordinal st ( for X being set
for n being Element of NAT st X c= Rank (the_rank_of x) holds
ex Y being set st
( Y c= Rank O & P₁[n,X,Y] ) ) holds
O1 c= O ) ) by A22;
( O1 c= O2 & O2 c= O1 ) by A27, A25;
hence y1 = y2 by A26, A24, XBOOLE_0:def 10; :: thesis:

end;

ex f being Function st
( dom f = NAT & f . 0 = the_rank_of F₁() & ( for n being Element of NAT holds S₁[n,f . n,f . (n + 1)] ) )

deffunc H₁( Element of NAT ) -> set = { k where k is Element of NAT : k <= $1 } ;
A28: for p, q being Function
for k being Element of NAT st dom p = H₁(k) & dom q = H₁(k + 1) & p . 0 = q . 0 & ( for n being Element of NAT st n < k holds
( S₁[n,p . n,p . (n + 1)] & S₁[n,q . n,q . (n + 1)] ) ) holds
p . k = q . k

let p, q be Function; :: thesis:
let k be Element of NAT ; :: thesis:
defpred S₂[ Element of NAT ] means ( $1 <= k implies p . $1 = q . $1 );
assume that
dom p = H₁(k) and
dom q = H₁(k + 1) and
A29: p . 0 = q . 0 and
A30: for n being Element of NAT st n < k holds
( S₁[n,p . n,p . (n + 1)] & S₁[n,q . n,q . (n + 1)] ) ; :: thesis:
A31: for n being Element of NAT st S₂[n] holds
S₂[n + 1]

let n be Element of NAT ; :: thesis:
assume A32: ( n <= k implies p . n = q . n ) ; :: thesis:
assume n + 1 <= k ; :: thesis:
then A33: n < k by NAT_1:13;
then A34: S₁[n,p . n,p . (n + 1)] by A30;
S₁[n,p . n,q . (n + 1)] by A30, A32, A33;
hence p . (n + 1) = q . (n + 1) by A21, A34; :: thesis:

end;

A35: S₂[ 0 ] by A29;
for n being Element of NAT holds S₂[n] from NAT_1:sch 1(A35, A31);
hence p . k = q . k ; :: thesis:

end;

A36: for n being Element of NAT ex p being Function st
( dom p = H₁(n) & p . 0 = the_rank_of F₁() & ( for k being Element of NAT st k < n holds
S₁[k,p . k,p . (k + 1)] ) )

defpred S₂[ Element of NAT ] means ex p being Function st
( dom p = H₁($1) & p . 0 = the_rank_of F₁() & ( for k being Element of NAT st k < $1 holds
S₁[k,p . k,p . (k + 1)] ) );
A37: for n being Element of NAT st S₂[n] holds
S₂[n + 1]

let n be Element of NAT ; :: thesis:
given p being Function such that dom p = H₁(n) and
A38: p . 0 = the_rank_of F₁() and
A39: for k being Element of NAT st k < n holds
S₁[k,p . k,p . (k + 1)] ; :: thesis:
consider z being set such that
A40: S₁[n,p . n,z] by A2;
defpred S₃[ set , set ] means for k being Element of NAT st k = $1 holds
( ( k <= n implies $2 = p . k ) & ( k = n + 1 implies $2 = z ) );
A41: for x being set st x in H₁(n + 1) holds
ex y being set st S₃[x,y]

let x be set ; :: thesis:
assume x in H₁(n + 1) ; :: thesis:
then A42: ex m being Element of NAT st
( m = x & m <= n + 1 ) ;
then reconsider t = x as Element of NAT ;
A43: ( t <= n implies ex y being set st S₃[x,y] )

assume A44: t <= n ; :: thesis:
take p . x ; :: thesis:
let k be Element of NAT ; :: thesis:
assume A45: k = x ; :: thesis:
hence ( k <= n implies p . x = p . k ) ; :: thesis:
assume k = n + 1 ; :: thesis:
then n + 1 <= n + 0 by A44, A45;
hence p . x = z by XREAL_1:8; :: thesis:

end;

( t = n + 1 implies ex y being set st S₃[x,y] )

assume A46: t = n + 1 ; :: thesis:
take z ; :: thesis:
let k be Element of NAT ; :: thesis:
assume A47: k = x ; :: thesis:
thus ( k <= n implies z = p . k ) :: thesis:

assume k <= n ; :: thesis:
then n + 1 <= n + 0 by A46, A47;
hence z = p . k by XREAL_1:8; :: thesis:

end;

thus ( k = n + 1 implies z = z ) ; :: thesis:

end;

hence ex y being set st S₃[x,y] by A42, A43, NAT_1:8; :: thesis:

end;

consider q being Function such that
A48: ( dom q = H₁(n + 1) & ( for x being set st x in H₁(n + 1) holds
S₃[x,q . x] ) ) from CLASSES1:sch 1(A41);
take q ; :: thesis:
thus dom q = H₁(n + 1) by A48; :: thesis:
0 in H₁(n + 1) ;
hence q . 0 = the_rank_of F₁() by A38, A48; :: thesis:
let k be Element of NAT ; :: thesis:
assume A49: k < n + 1 ; :: thesis:

A50: now

A51: k + 1 <= n + 1 by A49, NAT_1:13;
assume k <> n ; :: thesis:
then k + 1 <> n + 1 ;
then A52: k + 1 <= n by A51, NAT_1:8;
then A53: k < n by NAT_1:13;
k + 1 in H₁(n + 1) by A51;
then A54: q . (k + 1) = p . (k + 1) by A48, A52;
k in H₁(n + 1) by A49;
then p . k = q . k by A48, A53;
hence S₁[k,q . k,q . (k + 1)] by A39, A54, A53; :: thesis:

end;

assume A55: k = n ; :: thesis:
then k <= n + 1 by NAT_1:11;
then k in H₁(n + 1) ;
then A56: q . k = p . k by A48, A55;
k + 1 in H₁(n + 1) by A55;
then q . (k + 1) = z by A48, A55;
hence S₁[k,q . k,q . (k + 1)] by A40, A55, A56; :: thesis:

end;

hence S₁[k,q . k,q . (k + 1)] by A50; :: thesis:

end;

set s = H₁( 0 ) --> (the_rank_of F₁());
take H₁( 0 ) --> (the_rank_of F₁()) ; :: thesis:
thus dom (H₁( 0 ) --> (the_rank_of F₁())) = H₁( 0 ) by FUNCOP_1:19; :: thesis:
0 in H₁( 0 ) ;
hence (H₁( 0 ) --> (the_rank_of F₁())) . 0 = the_rank_of F₁() by FUNCOP_1:13; :: thesis:
thus for k being Element of NAT st k < 0 holds
S₁[k,(H₁( 0 ) --> (the_rank_of F₁())) . k,(H₁( 0 ) --> (the_rank_of F₁())) . (k + 1)] ; :: thesis:

end;

thus for n being Element of NAT holds S₂[n] from NAT_1:sch 1(A57, A37); :: thesis:

end;

ex f being Function st
( dom f = NAT & ( for n being Element of NAT ex p being Function st
( dom p = H₁(n) & p . 0 = the_rank_of F₁() & ( for k being Element of NAT st k < n holds
S₁[k,p . k,p . (k + 1)] ) & f . n = p . n ) ) )

defpred S₂[ set , set ] means for n being Element of NAT st n = $1 holds
ex p being Function st
( dom p = H₁(n) & p . 0 = the_rank_of F₁() & ( for k being Element of NAT st k < n holds
S₁[k,p . k,p . (k + 1)] ) & $2 = p . n );
A58: for x being set st x in NAT holds
ex y being set st S₂[x,y]

let x be set ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider n = x as Element of NAT ;
consider p being Function such that
A59: ( dom p = H₁(n) & p . 0 = the_rank_of F₁() & ( for k being Element of NAT st k < n holds
S₁[k,p . k,p . (k + 1)] ) ) by A36;
take p . n ; :: thesis:
let k be Element of NAT ; :: thesis:
assume A60: k = x ; :: thesis:
take p ; :: thesis:
thus ( dom p = H₁(k) & p . 0 = the_rank_of F₁() & ( for k being Element of NAT st k < k holds
S₁[k,p . k,p . (k + 1)] ) & p . n = p . k ) by A59, A60; :: thesis:

end;

consider f being Function such that
A61: ( dom f = NAT & ( for x being set st x in NAT holds
S₂[x,f . x] ) ) from CLASSES1:sch 1(A58);
take f ; :: thesis:
thus dom f = NAT by A61; :: thesis:
let n be Element of NAT ; :: thesis:
consider p being Function such that
A62: ( dom p = H₁(n) & p . 0 = the_rank_of F₁() ) and
A63: for k being Element of NAT st k < n holds
S₁[k,p . k,p . (k + 1)] and
A64: f . n = p . n by A61;
take p ; :: thesis:
thus ( dom p = H₁(n) & p . 0 = the_rank_of F₁() ) by A62; :: thesis:
thus for k being Element of NAT st k < n holds
S₁[k,p . k,p . (k + 1)] by A63; :: thesis:
thus f . n = p . n by A64; :: thesis:

end;

then consider f being Function such that
A65: dom f = NAT and
A66: for n being Element of NAT ex p being Function st
( dom p = H₁(n) & p . 0 = the_rank_of F₁() & ( for k being Element of NAT st k < n holds
S₁[k,p . k,p . (k + 1)] ) & f . n = p . n ) ;
take f ; :: thesis:
thus dom f = NAT by A65; :: thesis:
ex p being Function st
( dom p = H₁( 0 ) & p . 0 = the_rank_of F₁() & ( for k being Element of NAT st k < 0 holds
S₁[k,p . k,p . (k + 1)] ) & f . 0 = p . 0 ) by A66;
hence f . 0 = the_rank_of F₁() ; :: thesis:
let d be Element of NAT ; :: thesis:
consider p being Function such that
A67: dom p = H₁(d + 1) and
A68: p . 0 = the_rank_of F₁() and
A69: for k being Element of NAT st k < d + 1 holds
S₁[k,p . k,p . (k + 1)] and
A70: f . (d + 1) = p . (d + 1) by A66;
consider q being Function such that
A71: dom q = H₁(d) and
A72: q . 0 = the_rank_of F₁() and
A73: for k being Element of NAT st k < d holds
S₁[k,q . k,q . (k + 1)] and
A74: f . d = q . d by A66;
( dom p = H₁(d + 1) & dom q = H₁(d) & p . 0 = q . 0 & ( for k being Element of NAT st k < d holds
( S₁[k,q . k,q . (k + 1)] & S₁[k,p . k,p . (k + 1)] ) ) )

thus dom p = H₁(d + 1) by A67; :: thesis:
thus dom q = H₁(d) by A71; :: thesis:
thus p . 0 = q . 0 by A68, A72; :: thesis:
let k be Element of NAT ; :: thesis:
assume A75: k < d ; :: thesis:
hence S₁[k,q . k,q . (k + 1)] by A73; :: thesis:
d <= d + 1 by NAT_1:11;
then k < d + 1 by A75, XXREAL_0:2;
hence S₁[k,p . k,p . (k + 1)] by A69; :: thesis:

end;

then p . d = q . d by A28;
hence S₁[d,f . d,f . (d + 1)] by A69, A70, A74, XREAL_1:31; :: thesis:

end;

then consider g being Function such that
A76: dom g = NAT and
A77: g . 0 = the_rank_of F₁() and
A78: for n being Element of NAT holds S₁[n,g . n,g . (n + 1)] ;
defpred S₂[ set , set ] means ex i being Element of NAT st
( i = $1 `2 & P₁[$1 `2 ,$1 `1 ,$2 `1 ] & $2 `2 = i + 1 & ( for y being set holds
( not P₁[$1 `2 ,$1 `1 ,y] or not the_rank_of y in the_rank_of ($2 `1) ) ) );
A79: ( [F₁(),0] `1 = F₁() & [F₁(),0] `2 = 0 ) by MCART_1:7;
set beta = sup (rng g);
A80: for x being set st x in [:(Rank (sup (rng g))),NAT:] holds
ex u being set st S₂[x,u]

let x be set ; :: thesis:
defpred S₃[ Ordinal] means ex y being set st
( y c= Rank $1 & P₁[x `2 ,x `1 ,y] );
assume x in [:(Rank (sup (rng g))),NAT:] ; :: thesis:
then consider a, b being set such that
A81: a in Rank (sup (rng g)) and
A82: b in NAT and
A83: x = [a,b] by ZFMISC_1:def 2;
reconsider b = b as Element of NAT by A82;
A84: ( x `2 = b & x `1 = a ) by A83, MCART_1:7;
the_rank_of a in sup (rng g) by A81, CLASSES1:74;
then consider alfa being Ordinal such that
A85: alfa in rng g and
A86: the_rank_of a c= alfa by ORDINAL2:29;
consider k being set such that
A87: k in dom g and
A88: alfa = g . k by A85, FUNCT_1:def 5;
reconsider k = k as Element of NAT by A76, A87;
A89: S₁[k,alfa,g . (k + 1)] by A78, A88;
then reconsider O2 = g . (k + 1) as Ordinal ;
a c= Rank alfa by A86, CLASSES1:73;
then a c= Rank (the_rank_of alfa) by CLASSES1:81;
then ex y being set st
( y c= Rank O2 & P₁[x `2 ,x `1 ,y] ) by A89, A84;
then A90: ex O being Ordinal st S₃[O] ;
consider O being Ordinal such that
A91: S₃[O] and
A92: for O9 being Ordinal st S₃[O9] holds
O c= O9 from ORDINAL1:sch 1(A90);
consider Y being set such that
A93: Y c= Rank O and
A94: P₁[b,a,Y] by A84, A91;
A95: the_rank_of Y c= O by A93, CLASSES1:73;
take u = [Y,(b + 1)]; :: thesis:
take i = b; :: thesis:
thus i = x `2 by A83, MCART_1:7; :: thesis:
thus P₁[x `2 ,x `1 ,u `1 ] by A84, A94, MCART_1:7; :: thesis:
thus u `2 = i + 1 by MCART_1:7; :: thesis:
given y being set such that A96: P₁[x `2 ,x `1 ,y] and
A97: the_rank_of y in the_rank_of (u `1) ; :: thesis:
A98: y c= Rank (the_rank_of y) by CLASSES1:def 8;
the_rank_of y in the_rank_of Y by A97, MCART_1:7;
hence contradiction by A92, A96, A95, A98, ORDINAL1:7; :: thesis:

end;

consider F being Function such that
dom F = [:(Rank (sup (rng g))),NAT:] and
A99: for x being set st x in [:(Rank (sup (rng g))),NAT:] holds
S₂[x,F . x] from CLASSES1:sch 1(A80);
deffunc H₁( Nat, set ) -> set = (F . [$2,$1]) `1 ;
consider f being Function such that
A100: dom f = NAT and
A101: f . 0 = F₁() and
A102: for n being Nat holds f . (n + 1) = H₁(n,f . n) from NAT_1:sch 11();
defpred S₃[ Element of NAT ] means the_rank_of (f . $1) in sup (rng g);
g . 0 in rng g by A76, FUNCT_1:def 5;
then A103: S₃[ 0 ] by A77, A101, ORDINAL2:27;
A104: for n being Element of NAT st S₃[n] holds
S₃[n + 1]

let n be Element of NAT ; :: thesis:
assume A105: the_rank_of (f . n) in sup (rng g) ; :: thesis:
then consider o1 being Ordinal such that
A106: o1 in rng g and
A107: the_rank_of (f . n) c= o1 by ORDINAL2:29;
f . n in Rank (sup (rng g)) by A105, CLASSES1:74;
then A108: [(f . n),n] in [:(Rank (sup (rng g))),NAT:] by ZFMISC_1:106;
consider m being set such that
A109: m in dom g and
A110: g . m = o1 by A106, FUNCT_1:def 5;
reconsider m = m as Element of NAT by A76, A109;
consider o2 being Ordinal such that
A111: o2 = g . (m + 1) and
A112: for X being set
for n being Element of NAT st X c= Rank (the_rank_of (g . m)) holds
ex Y being set st
( Y c= Rank o2 & P₁[n,X,Y] ) and
for o being Ordinal st ( for X being set
for n being Element of NAT st X c= Rank (the_rank_of (g . m)) holds
ex Y being set st
( Y c= Rank o & P₁[n,X,Y] ) ) holds
o2 c= o by A78;
the_rank_of (f . n) c= the_rank_of (g . m) by A107, A110, CLASSES1:81;
then f . n c= Rank (the_rank_of (g . m)) by CLASSES1:73;
then consider YY being set such that
A113: YY c= Rank o2 and
A114: P₁[n,f . n,YY] by A112;
A115: the_rank_of YY c= o2 by A113, CLASSES1:73;
( [(f . n),n] `1 = f . n & [(f . n),n] `2 = n ) by MCART_1:7;
then ex i being Element of NAT st
( i = n & P₁[n,f . n,(F . [(f . n),n]) `1 ] & (F . [(f . n),n]) `2 = i + 1 & ( for y being set holds
( not P₁[n,f . n,y] or not the_rank_of y in the_rank_of ((F . [(f . n),n]) `1) ) ) ) by A99, A108;
then A116: the_rank_of ((F . [(f . n),n]) `1) c= the_rank_of YY by A114, ORDINAL1:26;
g . (m + 1) in rng g by A76, FUNCT_1:def 5;
then A117: o2 in sup (rng g) by A111, ORDINAL2:27;
f . (n + 1) = (F . [(f . n),n]) `1 by A102;
hence S₃[n + 1] by A116, A115, A117, ORDINAL1:22, XBOOLE_1:1; :: thesis:

end;

A118: for n being Element of NAT holds S₃[n] from NAT_1:sch 1(A103, A104);
defpred S₄[ Element of NAT ] means P₁[$1,f . $1,f . ($1 + 1)];
A119: for n being Element of NAT st S₄[n] holds
S₄[n + 1]

let n be Element of NAT ; :: thesis:
assume P₁[n,f . n,f . (n + 1)] ; :: thesis:
the_rank_of (f . (n + 1)) in sup (rng g) by A118;
then f . (n + 1) in Rank (sup (rng g)) by CLASSES1:74;
then A120: [(f . (n + 1)),(n + 1)] in [:(Rank (sup (rng g))),NAT:] by ZFMISC_1:106;
( [(f . (n + 1)),(n + 1)] `1 = f . (n + 1) & [(f . (n + 1)),(n + 1)] `2 = n + 1 ) by MCART_1:7;
then ex i being Element of NAT st
( i = n + 1 & P₁[n + 1,f . (n + 1),(F . [(f . (n + 1)),(n + 1)]) `1 ] & (F . [(f . (n + 1)),(n + 1)]) `2 = i + 1 & ( for y being set holds
( not P₁[n + 1,f . (n + 1),y] or not the_rank_of y in the_rank_of ((F . [(f . (n + 1)),(n + 1)]) `1) ) ) ) by A99, A120;
hence S₄[n + 1] by A102; :: thesis:

end;

take f ; :: thesis:
thus dom f = NAT by A100; :: thesis:
thus f . 0 = F₁() by A101; :: thesis:
F₁() in Rank (sup (rng g)) by A101, A103, CLASSES1:74;
then [F₁(),0] in [:(Rank (sup (rng g))),NAT:] by ZFMISC_1:106;
then ex i being Element of NAT st
( i = [F₁(),0] `2 & P₁[ 0 ,F₁(),(F . [F₁(),0]) `1 ] & (F . [F₁(),0]) `2 = i + 1 & ( for y being set holds
( not P₁[ 0 ,F₁(),y] or not the_rank_of y in the_rank_of ((F . [F₁(),0]) `1) ) ) ) by A99, A79;
then A121: S₄[ 0 ] by A101, A102;
thus for n being Element of NAT holds S₄[n] from NAT_1:sch 1(A121, A119); :: thesis: