defpred S1[ set , set , set ] means ex O2 being Ordinal st
( O2 = \$3 & ( for X being set
for n being Nat st X c= Rank () holds
ex Y being set st
( Y c= Rank O2 & P1[n,X,Y] ) ) & ( for O being Ordinal st ( for X being set
for n being Nat st X c= Rank () holds
ex Y being set st
( Y c= Rank O & P1[n,X,Y] ) ) holds
O2 c= O ) );
A2: for n being Nat
for x being set ex y being set st S1[n,x,y]
proof
defpred S2[ object , object ] means for m being Nat ex y being set st
( \$2 is Ordinal & y c= Rank () & P1[m,\$1,y] );
let n be Nat; :: thesis: for x being set ex y being set st S1[n,x,y]
let x be set ; :: thesis: ex y being set st S1[n,x,y]
defpred S3[ Ordinal] means for X being set
for n being Nat st X c= Rank () holds
ex Y being set st
( Y c= Rank \$1 & P1[n,X,Y] );
A3: for x9 being object st x9 in bool (Rank ()) holds
ex o being object st S2[x9,o]
proof
let x9 be object ; :: thesis: ( x9 in bool (Rank ()) implies ex o being object st S2[x9,o] )
assume x9 in bool (Rank ()) ; :: thesis: ex o being object st S2[x9,o]
defpred S4[ object , object ] means ex y being set st
( \$2 is Ordinal & y c= Rank () & P1[\$1,x9,y] );
A4: for e being object st e in NAT holds
ex u being object st S4[e,u]
proof
let i be object ; :: thesis: ( i in NAT implies ex u being object st S4[i,u] )
assume i in NAT ; :: thesis: ex u being object st S4[i,u]
then reconsider i9 = i as Nat ;
thus ex o being object ex y being set st
( o is Ordinal & y c= Rank () & P1[i,x9,y] ) :: thesis: verum
proof
x9 is set by TARSKI:1;
then consider y being set such that
A5: P1[i9,x9,y] by A1;
take o = the_rank_of y; :: thesis: ex y being set st
( o is Ordinal & y c= Rank () & P1[i,x9,y] )

take y ; :: thesis: ( o is Ordinal & y c= Rank () & P1[i,x9,y] )
thus o is Ordinal ; :: thesis: ( y c= Rank () & P1[i,x9,y] )
the_rank_of () = the_rank_of y by CLASSES1:73;
hence y c= Rank () by CLASSES1:65; :: thesis: P1[i,x9,y]
thus P1[i,x9,y] by A5; :: thesis: verum
end;
end;
consider h being Function such that
A6: dom h = NAT and
A7: for i being object st i in NAT holds
S4[i,h . i] from take o = sup (rng h); :: thesis: S2[x9,o]
thus for m being Nat ex y being set st
( o is Ordinal & y c= Rank () & P1[m,x9,y] ) :: thesis: verum
proof
let m be Nat; :: thesis: ex y being set st
( o is Ordinal & y c= Rank () & P1[m,x9,y] )

A8: m in NAT by ORDINAL1:def 12;
then consider y being set such that
A9: h . m is Ordinal and
A10: y c= Rank (the_rank_of (h . m)) and
A11: P1[m,x9,y] by A7;
reconsider O = h . m as Ordinal by A9;
h . m in rng h by ;
then h . m in sup (rng h) by ;
then h . m c= o by ORDINAL1:def 2;
then A12: Rank O c= Rank o by CLASSES1:37;
take y ; :: thesis: ( o is Ordinal & y c= Rank () & P1[m,x9,y] )
thus o is Ordinal ; :: thesis: ( y c= Rank () & P1[m,x9,y] )
y c= Rank O by ;
then y c= Rank o by A12;
hence y c= Rank () by CLASSES1:73; :: thesis: P1[m,x9,y]
thus P1[m,x9,y] by A11; :: thesis: verum
end;
end;
consider f being Function such that
A13: dom f = bool (Rank ()) and
A14: for x9 being object st x9 in bool (Rank ()) holds
S2[x9,f . x9] from A15: ex O being Ordinal st S3[O]
proof
take O2 = sup (rng f); :: thesis: S3[O2]
thus for X being set
for m being Nat st X c= Rank () holds
ex Y being set st
( Y c= Rank O2 & P1[m,X,Y] ) :: thesis: verum
proof
let X be set ; :: thesis: for m being Nat st X c= Rank () holds
ex Y being set st
( Y c= Rank O2 & P1[m,X,Y] )

let m be Nat; :: thesis: ( X c= Rank () implies ex Y being set st
( Y c= Rank O2 & P1[m,X,Y] ) )

assume A16: X c= Rank () ; :: thesis: ex Y being set st
( Y c= Rank O2 & P1[m,X,Y] )

then consider Y being set such that
A17: f . X is Ordinal and
A18: Y c= Rank (the_rank_of (f . X)) and
A19: P1[m,X,Y] by A14;
reconsider O = f . X as Ordinal by A17;
f . X in rng f by ;
then f . X in sup (rng f) by ;
then f . X c= O2 by ORDINAL1:def 2;
then A20: Rank O c= Rank O2 by CLASSES1:37;
take Y ; :: thesis: ( Y c= Rank O2 & P1[m,X,Y] )
the_rank_of O = O by CLASSES1:73;
hence Y c= Rank O2 by ; :: thesis: P1[m,X,Y]
thus P1[m,X,Y] by A19; :: thesis: verum
end;
end;
consider O2 being Ordinal such that
A21: ( S3[O2] & ( for O being Ordinal st S3[O] holds
O2 c= O ) ) from take O2 ; :: thesis: S1[n,x,O2]
thus S1[n,x,O2] by A21; :: thesis: verum
end;
A22: for n being Nat
for x, y1, y2 being set st S1[n,x,y1] & S1[n,x,y2] holds
y1 = y2
proof
let n be Nat; :: thesis: for x, y1, y2 being set st S1[n,x,y1] & S1[n,x,y2] holds
y1 = y2

let x, y1, y2 be set ; :: thesis: ( S1[n,x,y1] & S1[n,x,y2] implies y1 = y2 )
assume that
A23: S1[n,x,y1] and
A24: S1[n,x,y2] ; :: thesis: y1 = y2
consider O2 being Ordinal such that
A25: O2 = y2 and
A26: ( ( for X being set
for n being Nat st X c= Rank () holds
ex Y being set st
( Y c= Rank O2 & P1[n,X,Y] ) ) & ( for O being Ordinal st ( for X being set
for n being Nat st X c= Rank () holds
ex Y being set st
( Y c= Rank O & P1[n,X,Y] ) ) holds
O2 c= O ) ) by A24;
consider O1 being Ordinal such that
A27: O1 = y1 and
A28: ( ( for X being set
for n being Nat st X c= Rank () holds
ex Y being set st
( Y c= Rank O1 & P1[n,X,Y] ) ) & ( for O being Ordinal st ( for X being set
for n being Nat st X c= Rank () holds
ex Y being set st
( Y c= Rank O & P1[n,X,Y] ) ) holds
O1 c= O ) ) by A23;
( O1 c= O2 & O2 c= O1 ) by ;
hence y1 = y2 by ; :: thesis: verum
end;
ex f being Function st
( dom f = NAT & f . 0 = the_rank_of F1() & ( for n being Nat holds S1[n,f . n,f . (n + 1)] ) )
proof
deffunc H1( Nat) -> set = { k where k is Nat : k <= \$1 } ;
A29: for p, q being Function
for k being Nat st dom p = H1(k) & dom q = H1(k + 1) & p . 0 = q . 0 & ( for n being Nat st n < k holds
( S1[n,p . n,p . (n + 1)] & S1[n,q . n,q . (n + 1)] ) ) holds
p . k = q . k
proof
let p, q be Function; :: thesis: for k being Nat st dom p = H1(k) & dom q = H1(k + 1) & p . 0 = q . 0 & ( for n being Nat st n < k holds
( S1[n,p . n,p . (n + 1)] & S1[n,q . n,q . (n + 1)] ) ) holds
p . k = q . k

let k be Nat; :: thesis: ( dom p = H1(k) & dom q = H1(k + 1) & p . 0 = q . 0 & ( for n being Nat st n < k holds
( S1[n,p . n,p . (n + 1)] & S1[n,q . n,q . (n + 1)] ) ) implies p . k = q . k )

defpred S2[ Nat] means ( \$1 <= k implies p . \$1 = q . \$1 );
assume that
dom p = H1(k) and
dom q = H1(k + 1) and
A30: p . 0 = q . 0 and
A31: for n being Nat st n < k holds
( S1[n,p . n,p . (n + 1)] & S1[n,q . n,q . (n + 1)] ) ; :: thesis: p . k = q . k
A32: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A33: ( n <= k implies p . n = q . n ) ; :: thesis: S2[n + 1]
assume n + 1 <= k ; :: thesis: p . (n + 1) = q . (n + 1)
then A34: n < k by NAT_1:13;
then A35: S1[n,p . n,p . (n + 1)] by A31;
S1[n,p . n,q . (n + 1)] by ;
hence p . (n + 1) = q . (n + 1) by ; :: thesis: verum
end;
A36: S2[ 0 ] by A30;
for n being Nat holds S2[n] from hence p . k = q . k ; :: thesis: verum
end;
A37: for n being Nat ex p being Function st
( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Nat st k < n holds
S1[k,p . k,p . (k + 1)] ) )
proof
defpred S2[ Nat] means ex p being Function st
( dom p = H1(\$1) & p . 0 = the_rank_of F1() & ( for k being Nat st k < \$1 holds
S1[k,p . k,p . (k + 1)] ) );
A38: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
given p being Function such that dom p = H1(n) and
A39: p . 0 = the_rank_of F1() and
A40: for k being Nat st k < n holds
S1[k,p . k,p . (k + 1)] ; :: thesis: S2[n + 1]
consider z being set such that
A41: S1[n,p . n,z] by A2;
defpred S3[ object , object ] means for k being Nat st k = \$1 holds
( ( k <= n implies \$2 = p . k ) & ( k = n + 1 implies \$2 = z ) );
A42: for x being object st x in H1(n + 1) holds
ex y being object st S3[x,y]
proof
let x be object ; :: thesis: ( x in H1(n + 1) implies ex y being object st S3[x,y] )
assume x in H1(n + 1) ; :: thesis: ex y being object st S3[x,y]
then A43: ex m being Nat st
( m = x & m <= n + 1 ) ;
then reconsider t = x as Nat ;
A44: ( t <= n implies ex y being object st S3[x,y] )
proof
assume A45: t <= n ; :: thesis: ex y being object st S3[x,y]
take p . x ; :: thesis: S3[x,p . x]
let k be Nat; :: thesis: ( k = x implies ( ( k <= n implies p . x = p . k ) & ( k = n + 1 implies p . x = z ) ) )
assume A46: k = x ; :: thesis: ( ( k <= n implies p . x = p . k ) & ( k = n + 1 implies p . x = z ) )
hence ( k <= n implies p . x = p . k ) ; :: thesis: ( k = n + 1 implies p . x = z )
assume k = n + 1 ; :: thesis: p . x = z
then n + 1 <= n + 0 by ;
hence p . x = z by XREAL_1:6; :: thesis: verum
end;
( t = n + 1 implies ex y being object st S3[x,y] )
proof
assume A47: t = n + 1 ; :: thesis: ex y being object st S3[x,y]
take z ; :: thesis: S3[x,z]
let k be Nat; :: thesis: ( k = x implies ( ( k <= n implies z = p . k ) & ( k = n + 1 implies z = z ) ) )
assume A48: k = x ; :: thesis: ( ( k <= n implies z = p . k ) & ( k = n + 1 implies z = z ) )
thus ( k <= n implies z = p . k ) :: thesis: ( k = n + 1 implies z = z )
proof
assume k <= n ; :: thesis: z = p . k
then n + 1 <= n + 0 by ;
hence z = p . k by XREAL_1:6; :: thesis: verum
end;
thus ( k = n + 1 implies z = z ) ; :: thesis: verum
end;
hence ex y being object st S3[x,y] by ; :: thesis: verum
end;
consider q being Function such that
A49: ( dom q = H1(n + 1) & ( for x being object st x in H1(n + 1) holds
S3[x,q . x] ) ) from take q ; :: thesis: ( dom q = H1(n + 1) & q . 0 = the_rank_of F1() & ( for k being Nat st k < n + 1 holds
S1[k,q . k,q . (k + 1)] ) )

thus dom q = H1(n + 1) by A49; :: thesis: ( q . 0 = the_rank_of F1() & ( for k being Nat st k < n + 1 holds
S1[k,q . k,q . (k + 1)] ) )

0 in H1(n + 1) ;
hence q . 0 = the_rank_of F1() by ; :: thesis: for k being Nat st k < n + 1 holds
S1[k,q . k,q . (k + 1)]

let k be Nat; :: thesis: ( k < n + 1 implies S1[k,q . k,q . (k + 1)] )
assume A50: k < n + 1 ; :: thesis: S1[k,q . k,q . (k + 1)]
A51: now :: thesis: ( k <> n implies S1[k,q . k,q . (k + 1)] )
A52: k + 1 <= n + 1 by ;
assume k <> n ; :: thesis: S1[k,q . k,q . (k + 1)]
then k + 1 <> n + 1 ;
then A53: k + 1 <= n by ;
then A54: k < n by NAT_1:13;
k + 1 in H1(n + 1) by A52;
then A55: q . (k + 1) = p . (k + 1) by ;
k in H1(n + 1) by A50;
then p . k = q . k by ;
hence S1[k,q . k,q . (k + 1)] by ; :: thesis: verum
end;
now :: thesis: ( k = n implies S1[k,q . k,q . (k + 1)] )
assume A56: k = n ; :: thesis: S1[k,q . k,q . (k + 1)]
then k <= n + 1 by NAT_1:11;
then k in H1(n + 1) ;
then A57: q . k = p . k by ;
k + 1 in H1(n + 1) by A56;
then q . (k + 1) = z by ;
hence S1[k,q . k,q . (k + 1)] by ; :: thesis: verum
end;
hence S1[k,q . k,q . (k + 1)] by A51; :: thesis: verum
end;
A58: S2[ 0 ]
proof
set s = H1( 0 ) --> (the_rank_of F1());
take H1( 0 ) --> (the_rank_of F1()) ; :: thesis: ( dom (H1( 0 ) --> (the_rank_of F1())) = H1( 0 ) & (H1( 0 ) --> (the_rank_of F1())) . 0 = the_rank_of F1() & ( for k being Nat st k < 0 holds
S1[k,(H1( 0 ) --> (the_rank_of F1())) . k,(H1( 0 ) --> (the_rank_of F1())) . (k + 1)] ) )

thus dom (H1( 0 ) --> (the_rank_of F1())) = H1( 0 ) by FUNCOP_1:13; :: thesis: ( (H1( 0 ) --> (the_rank_of F1())) . 0 = the_rank_of F1() & ( for k being Nat st k < 0 holds
S1[k,(H1( 0 ) --> (the_rank_of F1())) . k,(H1( 0 ) --> (the_rank_of F1())) . (k + 1)] ) )

0 in H1( 0 ) ;
hence (H1( 0 ) --> (the_rank_of F1())) . 0 = the_rank_of F1() by FUNCOP_1:7; :: thesis: for k being Nat st k < 0 holds
S1[k,(H1( 0 ) --> (the_rank_of F1())) . k,(H1( 0 ) --> (the_rank_of F1())) . (k + 1)]

thus for k being Nat st k < 0 holds
S1[k,(H1( 0 ) --> (the_rank_of F1())) . k,(H1( 0 ) --> (the_rank_of F1())) . (k + 1)] ; :: thesis: verum
end;
thus for n being Nat holds S2[n] from :: thesis: verum
end;
ex f being Function st
( dom f = NAT & ( for n being Nat ex p being Function st
( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Nat st k < n holds
S1[k,p . k,p . (k + 1)] ) & f . n = p . n ) ) )
proof
defpred S2[ object , object ] means for n being Nat st n = \$1 holds
ex p being Function st
( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Nat st k < n holds
S1[k,p . k,p . (k + 1)] ) & \$2 = p . n );
A59: for x being object st x in NAT holds
ex y being object st S2[x,y]
proof
let x be object ; :: thesis: ( x in NAT implies ex y being object st S2[x,y] )
assume x in NAT ; :: thesis: ex y being object st S2[x,y]
then reconsider n = x as Nat ;
consider p being Function such that
A60: ( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Nat st k < n holds
S1[k,p . k,p . (k + 1)] ) ) by A37;
take p . n ; :: thesis: S2[x,p . n]
let k be Nat; :: thesis: ( k = x implies ex p being Function st
( dom p = H1(k) & p . 0 = the_rank_of F1() & ( for k being Nat st k < k holds
S1[k,p . k,p . (k + 1)] ) & p . n = p . k ) )

assume A61: k = x ; :: thesis: ex p being Function st
( dom p = H1(k) & p . 0 = the_rank_of F1() & ( for k being Nat st k < k holds
S1[k,p . k,p . (k + 1)] ) & p . n = p . k )

take p ; :: thesis: ( dom p = H1(k) & p . 0 = the_rank_of F1() & ( for k being Nat st k < k holds
S1[k,p . k,p . (k + 1)] ) & p . n = p . k )

thus ( dom p = H1(k) & p . 0 = the_rank_of F1() & ( for k being Nat st k < k holds
S1[k,p . k,p . (k + 1)] ) & p . n = p . k ) by ; :: thesis: verum
end;
consider f being Function such that
A62: ( dom f = NAT & ( for x being object st x in NAT holds
S2[x,f . x] ) ) from take f ; :: thesis: ( dom f = NAT & ( for n being Nat ex p being Function st
( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Nat st k < n holds
S1[k,p . k,p . (k + 1)] ) & f . n = p . n ) ) )

thus dom f = NAT by A62; :: thesis: for n being Nat ex p being Function st
( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Nat st k < n holds
S1[k,p . k,p . (k + 1)] ) & f . n = p . n )

let n be Nat; :: thesis: ex p being Function st
( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Nat st k < n holds
S1[k,p . k,p . (k + 1)] ) & f . n = p . n )

n in NAT by ORDINAL1:def 12;
then consider p being Function such that
A63: ( dom p = H1(n) & p . 0 = the_rank_of F1() ) and
A64: for k being Nat st k < n holds
S1[k,p . k,p . (k + 1)] and
A65: f . n = p . n by A62;
take p ; :: thesis: ( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Nat st k < n holds
S1[k,p . k,p . (k + 1)] ) & f . n = p . n )

thus ( dom p = H1(n) & p . 0 = the_rank_of F1() ) by A63; :: thesis: ( ( for k being Nat st k < n holds
S1[k,p . k,p . (k + 1)] ) & f . n = p . n )

thus for k being Nat st k < n holds
S1[k,p . k,p . (k + 1)] by A64; :: thesis: f . n = p . n
thus f . n = p . n by A65; :: thesis: verum
end;
then consider f being Function such that
A66: dom f = NAT and
A67: for n being Nat ex p being Function st
( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Nat st k < n holds
S1[k,p . k,p . (k + 1)] ) & f . n = p . n ) ;
take f ; :: thesis: ( dom f = NAT & f . 0 = the_rank_of F1() & ( for n being Nat holds S1[n,f . n,f . (n + 1)] ) )
thus dom f = NAT by A66; :: thesis: ( f . 0 = the_rank_of F1() & ( for n being Nat holds S1[n,f . n,f . (n + 1)] ) )
ex p being Function st
( dom p = H1( 0 ) & p . 0 = the_rank_of F1() & ( for k being Nat st k < 0 holds
S1[k,p . k,p . (k + 1)] ) & f . 0 = p . 0 ) by A67;
hence f . 0 = the_rank_of F1() ; :: thesis: for n being Nat holds S1[n,f . n,f . (n + 1)]
let d be Nat; :: thesis: S1[d,f . d,f . (d + 1)]
consider p being Function such that
A68: dom p = H1(d + 1) and
A69: p . 0 = the_rank_of F1() and
A70: for k being Nat st k < d + 1 holds
S1[k,p . k,p . (k + 1)] and
A71: f . (d + 1) = p . (d + 1) by A67;
consider q being Function such that
A72: dom q = H1(d) and
A73: q . 0 = the_rank_of F1() and
A74: for k being Nat st k < d holds
S1[k,q . k,q . (k + 1)] and
A75: f . d = q . d by A67;
( dom p = H1(d + 1) & dom q = H1(d) & p . 0 = q . 0 & ( for k being Nat st k < d holds
( S1[k,q . k,q . (k + 1)] & S1[k,p . k,p . (k + 1)] ) ) )
proof
thus dom p = H1(d + 1) by A68; :: thesis: ( dom q = H1(d) & p . 0 = q . 0 & ( for k being Nat st k < d holds
( S1[k,q . k,q . (k + 1)] & S1[k,p . k,p . (k + 1)] ) ) )

thus dom q = H1(d) by A72; :: thesis: ( p . 0 = q . 0 & ( for k being Nat st k < d holds
( S1[k,q . k,q . (k + 1)] & S1[k,p . k,p . (k + 1)] ) ) )

thus p . 0 = q . 0 by ; :: thesis: for k being Nat st k < d holds
( S1[k,q . k,q . (k + 1)] & S1[k,p . k,p . (k + 1)] )

let k be Nat; :: thesis: ( k < d implies ( S1[k,q . k,q . (k + 1)] & S1[k,p . k,p . (k + 1)] ) )
assume A76: k < d ; :: thesis: ( S1[k,q . k,q . (k + 1)] & S1[k,p . k,p . (k + 1)] )
hence S1[k,q . k,q . (k + 1)] by A74; :: thesis: S1[k,p . k,p . (k + 1)]
d <= d + 1 by NAT_1:11;
then k < d + 1 by ;
hence S1[k,p . k,p . (k + 1)] by A70; :: thesis: verum
end;
then p . d = q . d by A29;
hence S1[d,f . d,f . (d + 1)] by ; :: thesis: verum
end;
then consider g being Function such that
A77: dom g = NAT and
A78: g . 0 = the_rank_of F1() and
A79: for n being Nat holds S1[n,g . n,g . (n + 1)] ;
defpred S2[ object , object ] means ex i being Nat st
( i = \$1 `2 & P1[\$1 `2 ,\$1 `1 ,\$2 `1 ] & \$2 `2 = i + 1 & ( for y being set holds
( not P1[\$1 `2 ,\$1 `1 ,y] or not the_rank_of y in the_rank_of (\$2 `1) ) ) );
A80: ( [F1(),0] `1 = F1() & [F1(),0] `2 = 0 ) ;
set beta = sup (rng g);
A81: for x being object st x in [:(Rank (sup (rng g))),NAT:] holds
ex u being object st S2[x,u]
proof
let x be object ; :: thesis: ( x in [:(Rank (sup (rng g))),NAT:] implies ex u being object st S2[x,u] )
defpred S3[ Ordinal] means ex y being set st
( y c= Rank \$1 & P1[x `2 ,x `1 ,y] );
assume x in [:(Rank (sup (rng g))),NAT:] ; :: thesis: ex u being object st S2[x,u]
then consider a, b being object such that
A82: a in Rank (sup (rng g)) and
A83: b in NAT and
A84: x = [a,b] by ZFMISC_1:def 2;
reconsider b = b as Nat by A83;
A85: ( x `2 = b & x `1 = a ) by A84;
the_rank_of a in sup (rng g) by ;
then consider alfa being Ordinal such that
A86: alfa in rng g and
A87: the_rank_of a c= alfa by ORDINAL2:21;
consider k being object such that
A88: k in dom g and
A89: alfa = g . k by ;
reconsider k = k as Nat by ;
A90: S1[k,alfa,g . (k + 1)] by ;
then reconsider O2 = g . (k + 1) as Ordinal ;
reconsider a = a as set by TARSKI:1;
a c= Rank alfa by ;
then a c= Rank (the_rank_of alfa) by CLASSES1:73;
then ex y being set st
( y c= Rank O2 & P1[x `2 ,x `1 ,y] ) by ;
then A91: ex O being Ordinal st S3[O] ;
consider O being Ordinal such that
A92: S3[O] and
A93: for O9 being Ordinal st S3[O9] holds
O c= O9 from consider Y being set such that
A94: Y c= Rank O and
A95: P1[b,a,Y] by A85, A92;
A96: the_rank_of Y c= O by ;
take u = [Y,(b + 1)]; :: thesis: S2[x,u]
take i = b; :: thesis: ( i = x `2 & P1[x `2 ,x `1 ,u `1 ] & u `2 = i + 1 & ( for y being set holds
( not P1[x `2 ,x `1 ,y] or not the_rank_of y in the_rank_of (u `1) ) ) )

thus i = x `2 by A84; :: thesis: ( P1[x `2 ,x `1 ,u `1 ] & u `2 = i + 1 & ( for y being set holds
( not P1[x `2 ,x `1 ,y] or not the_rank_of y in the_rank_of (u `1) ) ) )

thus P1[x `2 ,x `1 ,u `1 ] by ; :: thesis: ( u `2 = i + 1 & ( for y being set holds
( not P1[x `2 ,x `1 ,y] or not the_rank_of y in the_rank_of (u `1) ) ) )

thus u `2 = i + 1 ; :: thesis: for y being set holds
( not P1[x `2 ,x `1 ,y] or not the_rank_of y in the_rank_of (u `1) )

given y being set such that A97: P1[x `2 ,x `1 ,y] and
A98: the_rank_of y in the_rank_of (u `1) ; :: thesis: contradiction
A99: y c= Rank () by CLASSES1:def 9;
the_rank_of y in the_rank_of Y by A98;
hence contradiction by A93, A97, A96, A99, ORDINAL1:5; :: thesis: verum
end;
consider F being Function such that
dom F = [:(Rank (sup (rng g))),NAT:] and
A100: for x being object st x in [:(Rank (sup (rng g))),NAT:] holds
S2[x,F . x] from deffunc H1( Nat, set ) -> object = (F . [\$2,\$1]) `1 ;
consider f being Function such that
A101: dom f = NAT and
A102: f . 0 = F1() and
A103: for n being Nat holds f . (n + 1) = H1(n,f . n) from NAT_1:sch 11();
defpred S3[ Nat] means the_rank_of (f . \$1) in sup (rng g);
g . 0 in rng g by ;
then A104: S3[ 0 ] by ;
A105: for n being Nat st S3[n] holds
S3[n + 1]
proof
let n be Nat; :: thesis: ( S3[n] implies S3[n + 1] )
assume A106: the_rank_of (f . n) in sup (rng g) ; :: thesis: S3[n + 1]
then consider o1 being Ordinal such that
A107: o1 in rng g and
A108: the_rank_of (f . n) c= o1 by ORDINAL2:21;
A109: n in NAT by ORDINAL1:def 12;
f . n in Rank (sup (rng g)) by ;
then A110: [(f . n),n] in [:(Rank (sup (rng g))),NAT:] by ;
consider m being object such that
A111: m in dom g and
A112: g . m = o1 by ;
reconsider m = m as Nat by ;
consider o2 being Ordinal such that
A113: o2 = g . (m + 1) and
A114: for X being set
for n being Nat st X c= Rank (the_rank_of (g . m)) holds
ex Y being set st
( Y c= Rank o2 & P1[n,X,Y] ) and
for o being Ordinal st ( for X being set
for n being Nat st X c= Rank (the_rank_of (g . m)) holds
ex Y being set st
( Y c= Rank o & P1[n,X,Y] ) ) holds
o2 c= o by A79;
the_rank_of (f . n) c= the_rank_of (g . m) by ;
then f . n c= Rank (the_rank_of (g . m)) by CLASSES1:65;
then consider YY being set such that
A115: YY c= Rank o2 and
A116: P1[n,f . n,YY] by A114;
A117: the_rank_of YY c= o2 by ;
( [(f . n),n] `1 = f . n & [(f . n),n] `2 = n ) ;
then ex i being Nat st
( i = n & P1[n,f . n,(F . [(f . n),n]) `1 ] & (F . [(f . n),n]) `2 = i + 1 & ( for y being set holds
( not P1[n,f . n,y] or not the_rank_of y in the_rank_of ((F . [(f . n),n]) `1) ) ) ) by ;
then A118: the_rank_of ((F . [(f . n),n]) `1) c= the_rank_of YY by ;
g . (m + 1) in rng g by ;
then A119: o2 in sup (rng g) by ;
f . (n + 1) = (F . [(f . n),n]) `1 by A103;
hence S3[n + 1] by ; :: thesis: verum
end;
A120: for n being Nat holds S3[n] from defpred S4[ Nat] means P1[\$1,f . \$1,f . (\$1 + 1)];
A121: for n being Nat st S4[n] holds
S4[n + 1]
proof
let n be Nat; :: thesis: ( S4[n] implies S4[n + 1] )
assume P1[n,f . n,f . (n + 1)] ; :: thesis: S4[n + 1]
the_rank_of (f . (n + 1)) in sup (rng g) by A120;
then f . (n + 1) in Rank (sup (rng g)) by CLASSES1:66;
then A122: [(f . (n + 1)),(n + 1)] in [:(Rank (sup (rng g))),NAT:] by ZFMISC_1:87;
( [(f . (n + 1)),(n + 1)] `1 = f . (n + 1) & [(f . (n + 1)),(n + 1)] `2 = n + 1 ) ;
then ex i being Nat st
( i = n + 1 & P1[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 P1[n + 1,f . (n + 1),y] or not the_rank_of y in the_rank_of ((F . [(f . (n + 1)),(n + 1)]) `1) ) ) ) by ;
hence S4[n + 1] by A103; :: thesis: verum
end;
take f ; :: thesis: ( dom f = NAT & f . 0 = F1() & ( for n being Nat holds P1[n,f . n,f . (n + 1)] ) )
thus dom f = NAT by A101; :: thesis: ( f . 0 = F1() & ( for n being Nat holds P1[n,f . n,f . (n + 1)] ) )
thus f . 0 = F1() by A102; :: thesis: for n being Nat holds P1[n,f . n,f . (n + 1)]
F1() in Rank (sup (rng g)) by ;
then [F1(),0] in [:(Rank (sup (rng g))),NAT:] by ZFMISC_1:87;
then ex i being Nat st
( i = [F1(),0] `2 & P1[ 0 ,F1(),(F . [F1(),0]) `1 ] & (F . [F1(),0]) `2 = i + 1 & ( for y being set holds
( not P1[ 0 ,F1(),y] or not the_rank_of y in the_rank_of ((F . [F1(),0]) `1) ) ) ) by ;
then A123: S4[ 0 ] by ;
thus for n being Nat holds S4[n] from :: thesis: verum