defpred S_{1}[ set , set , set ] means ex O2 being Ordinal st

( O2 = $3 & ( for X being set

for n being Nat st X c= Rank (the_rank_of $2) holds

ex Y being set st

( Y c= Rank O2 & P_{1}[n,X,Y] ) ) & ( for O being Ordinal st ( for X being set

for n being Nat st X c= Rank (the_rank_of $2) holds

ex Y being set st

( Y c= Rank O & P_{1}[n,X,Y] ) ) holds

O2 c= O ) );

A2: for n being Nat

for x being set ex y being set st S_{1}[n,x,y]

for x, y1, y2 being set st S_{1}[n,x,y1] & S_{1}[n,x,y2] holds

y1 = y2

( dom f = NAT & f . 0 = the_rank_of F_{1}() & ( for n being Nat holds S_{1}[n,f . n,f . (n + 1)] ) )

A77: dom g = NAT and

A78: g . 0 = the_rank_of F_{1}()
and

A79: for n being Nat holds S_{1}[n,g . n,g . (n + 1)]
;

defpred S_{2}[ object , object ] means ex i being Nat st

( i = $1 `2 & P_{1}[$1 `2 ,$1 `1 ,$2 `1 ] & $2 `2 = i + 1 & ( for y being set holds

( not P_{1}[$1 `2 ,$1 `1 ,y] or not the_rank_of y in the_rank_of ($2 `1) ) ) );

A80: ( [F_{1}(),0] `1 = F_{1}() & [F_{1}(),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 S_{2}[x,u]

dom F = [:(Rank (sup (rng g))),NAT:] and

A100: for x being object st x in [:(Rank (sup (rng g))),NAT:] holds

S_{2}[x,F . x]
from CLASSES1:sch 1(A81);

deffunc H_{1}( Nat, set ) -> object = (F . [$2,$1]) `1 ;

consider f being Function such that

A101: dom f = NAT and

A102: f . 0 = F_{1}()
and

A103: for n being Nat holds f . (n + 1) = H_{1}(n,f . n)
from NAT_1:sch 11();

defpred S_{3}[ Nat] means the_rank_of (f . $1) in sup (rng g);

g . 0 in rng g by A77, FUNCT_1:def 3;

then A104: S_{3}[ 0 ]
by A78, A102, ORDINAL2:19;

A105: for n being Nat st S_{3}[n] holds

S_{3}[n + 1]
_{3}[n]
from NAT_1:sch 2(A104, A105);

defpred S_{4}[ Nat] means P_{1}[$1,f . $1,f . ($1 + 1)];

A121: for n being Nat st S_{4}[n] holds

S_{4}[n + 1]
_{1}() & ( for n being Nat holds P_{1}[n,f . n,f . (n + 1)] ) )

thus dom f = NAT by A101; :: thesis: ( f . 0 = F_{1}() & ( for n being Nat holds P_{1}[n,f . n,f . (n + 1)] ) )

thus f . 0 = F_{1}()
by A102; :: thesis: for n being Nat holds P_{1}[n,f . n,f . (n + 1)]

F_{1}() in Rank (sup (rng g))
by A102, A104, CLASSES1:66;

then [F_{1}(),0] in [:(Rank (sup (rng g))),NAT:]
by ZFMISC_1:87;

then ex i being Nat st

( i = [F_{1}(),0] `2 & P_{1}[ 0 ,F_{1}(),(F . [F_{1}(),0]) `1 ] & (F . [F_{1}(),0]) `2 = i + 1 & ( for y being set holds

( not P_{1}[ 0 ,F_{1}(),y] or not the_rank_of y in the_rank_of ((F . [F_{1}(),0]) `1) ) ) )
by A100, A80;

then A123: S_{4}[ 0 ]
by A102, A103;

thus for n being Nat holds S_{4}[n]
from NAT_1:sch 2(A123, A121); :: thesis: verum

( O2 = $3 & ( for X being set

for n being Nat st X c= Rank (the_rank_of $2) holds

ex Y being set st

( Y c= Rank O2 & P

for n being Nat st X c= Rank (the_rank_of $2) holds

ex Y being set st

( Y c= Rank O & P

O2 c= O ) );

A2: for n being Nat

for x being set ex y being set st S

proof

A22:
for n being Nat
defpred S_{2}[ object , object ] means for m being Nat ex y being set st

( $2 is Ordinal & y c= Rank (the_rank_of $2) & P_{1}[m,$1,y] );

let n be Nat; :: thesis: for x being set ex y being set st S_{1}[n,x,y]

let x be set ; :: thesis: ex y being set st S_{1}[n,x,y]

defpred S_{3}[ Ordinal] means for X being set

for n being Nat st X c= Rank (the_rank_of x) holds

ex Y being set st

( Y c= Rank $1 & P_{1}[n,X,Y] );

A3: for x9 being object st x9 in bool (Rank (the_rank_of x)) holds

ex o being object st S_{2}[x9,o]

A13: dom f = bool (Rank (the_rank_of x)) and

A14: for x9 being object st x9 in bool (Rank (the_rank_of x)) holds

S_{2}[x9,f . x9]
from CLASSES1:sch 1(A3);

A15: ex O being Ordinal st S_{3}[O]

A21: ( S_{3}[O2] & ( for O being Ordinal st S_{3}[O] holds

O2 c= O ) ) from ORDINAL1:sch 1(A15);

take O2 ; :: thesis: S_{1}[n,x,O2]

thus S_{1}[n,x,O2]
by A21; :: thesis: verum

end;( $2 is Ordinal & y c= Rank (the_rank_of $2) & P

let n be Nat; :: thesis: for x being set ex y being set st S

let x be set ; :: thesis: ex y being set st S

defpred S

for n being Nat st X c= Rank (the_rank_of x) holds

ex Y being set st

( Y c= Rank $1 & P

A3: for x9 being object st x9 in bool (Rank (the_rank_of x)) holds

ex o being object st S

proof

consider f being Function such that
let x9 be object ; :: thesis: ( x9 in bool (Rank (the_rank_of x)) implies ex o being object st S_{2}[x9,o] )

assume x9 in bool (Rank (the_rank_of x)) ; :: thesis: ex o being object st S_{2}[x9,o]

defpred S_{4}[ object , object ] means ex y being set st

( $2 is Ordinal & y c= Rank (the_rank_of $2) & P_{1}[$1,x9,y] );

A4: for e being object st e in NAT holds

ex u being object st S_{4}[e,u]

A6: dom h = NAT and

A7: for i being object st i in NAT holds

S_{4}[i,h . i]
from CLASSES1:sch 1(A4);

take o = sup (rng h); :: thesis: S_{2}[x9,o]

thus for m being Nat ex y being set st

( o is Ordinal & y c= Rank (the_rank_of o) & P_{1}[m,x9,y] )
:: thesis: verum

end;assume x9 in bool (Rank (the_rank_of x)) ; :: thesis: ex o being object st S

defpred S

( $2 is Ordinal & y c= Rank (the_rank_of $2) & P

A4: for e being object st e in NAT holds

ex u being object st S

proof

consider h being Function such that
let i be object ; :: thesis: ( i in NAT implies ex u being object st S_{4}[i,u] )

assume i in NAT ; :: thesis: ex u being object st S_{4}[i,u]

then reconsider i9 = i as Nat ;

thus ex o being object ex y being set st

( o is Ordinal & y c= Rank (the_rank_of o) & P_{1}[i,x9,y] )
:: thesis: verum

end;assume i in NAT ; :: thesis: ex u being object st S

then reconsider i9 = i as Nat ;

thus ex o being object ex y being set st

( o is Ordinal & y c= Rank (the_rank_of o) & P

proof

x9 is set
by TARSKI:1;

then consider y being set such that

A5: P_{1}[i9,x9,y]
by A1;

take o = the_rank_of y; :: thesis: ex y being set st

( o is Ordinal & y c= Rank (the_rank_of o) & P_{1}[i,x9,y] )

take y ; :: thesis: ( o is Ordinal & y c= Rank (the_rank_of o) & P_{1}[i,x9,y] )

thus o is Ordinal ; :: thesis: ( y c= Rank (the_rank_of o) & P_{1}[i,x9,y] )

the_rank_of (the_rank_of y) = the_rank_of y by CLASSES1:73;

hence y c= Rank (the_rank_of o) by CLASSES1:65; :: thesis: P_{1}[i,x9,y]

thus P_{1}[i,x9,y]
by A5; :: thesis: verum

end;then consider y being set such that

A5: P

take o = the_rank_of y; :: thesis: ex y being set st

( o is Ordinal & y c= Rank (the_rank_of o) & P

take y ; :: thesis: ( o is Ordinal & y c= Rank (the_rank_of o) & P

thus o is Ordinal ; :: thesis: ( y c= Rank (the_rank_of o) & P

the_rank_of (the_rank_of y) = the_rank_of y by CLASSES1:73;

hence y c= Rank (the_rank_of o) by CLASSES1:65; :: thesis: P

thus P

A6: dom h = NAT and

A7: for i being object st i in NAT holds

S

take o = sup (rng h); :: thesis: S

thus for m being Nat ex y being set st

( o is Ordinal & y c= Rank (the_rank_of o) & P

proof

let m be Nat; :: thesis: ex y being set st

( o is Ordinal & y c= Rank (the_rank_of o) & P_{1}[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: P_{1}[m,x9,y]
by A7;

reconsider O = h . m as Ordinal by A9;

h . m in rng h by A6, A8, FUNCT_1:def 3;

then h . m in sup (rng h) by A9, ORDINAL2:19;

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 (the_rank_of o) & P_{1}[m,x9,y] )

thus o is Ordinal ; :: thesis: ( y c= Rank (the_rank_of o) & P_{1}[m,x9,y] )

y c= Rank O by A10, CLASSES1:73;

then y c= Rank o by A12;

hence y c= Rank (the_rank_of o) by CLASSES1:73; :: thesis: P_{1}[m,x9,y]

thus P_{1}[m,x9,y]
by A11; :: thesis: verum

end;( o is Ordinal & y c= Rank (the_rank_of o) & P

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: P

reconsider O = h . m as Ordinal by A9;

h . m in rng h by A6, A8, FUNCT_1:def 3;

then h . m in sup (rng h) by A9, ORDINAL2:19;

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 (the_rank_of o) & P

thus o is Ordinal ; :: thesis: ( y c= Rank (the_rank_of o) & P

y c= Rank O by A10, CLASSES1:73;

then y c= Rank o by A12;

hence y c= Rank (the_rank_of o) by CLASSES1:73; :: thesis: P

thus P

A13: dom f = bool (Rank (the_rank_of x)) and

A14: for x9 being object st x9 in bool (Rank (the_rank_of x)) holds

S

A15: ex O being Ordinal st S

proof

consider O2 being Ordinal such that
take O2 = sup (rng f); :: thesis: S_{3}[O2]

thus for X being set

for m being Nat st X c= Rank (the_rank_of x) holds

ex Y being set st

( Y c= Rank O2 & P_{1}[m,X,Y] )
:: thesis: verum

end;thus for X being set

for m being Nat st X c= Rank (the_rank_of x) holds

ex Y being set st

( Y c= Rank O2 & P

proof

let X be set ; :: thesis: for m being Nat st X c= Rank (the_rank_of x) holds

ex Y being set st

( Y c= Rank O2 & P_{1}[m,X,Y] )

let m be Nat; :: thesis: ( X c= Rank (the_rank_of x) implies ex Y being set st

( Y c= Rank O2 & P_{1}[m,X,Y] ) )

assume A16: X c= Rank (the_rank_of x) ; :: thesis: ex Y being set st

( Y c= Rank O2 & P_{1}[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: P_{1}[m,X,Y]
by A14;

reconsider O = f . X as Ordinal by A17;

f . X in rng f by A13, A16, FUNCT_1:def 3;

then f . X in sup (rng f) by A17, ORDINAL2:19;

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 & P_{1}[m,X,Y] )

the_rank_of O = O by CLASSES1:73;

hence Y c= Rank O2 by A18, A20; :: thesis: P_{1}[m,X,Y]

thus P_{1}[m,X,Y]
by A19; :: thesis: verum

end;ex Y being set st

( Y c= Rank O2 & P

let m be Nat; :: thesis: ( X c= Rank (the_rank_of x) implies ex Y being set st

( Y c= Rank O2 & P

assume A16: X c= Rank (the_rank_of x) ; :: thesis: ex Y being set st

( Y c= Rank O2 & P

then consider Y being set such that

A17: f . X is Ordinal and

A18: Y c= Rank (the_rank_of (f . X)) and

A19: P

reconsider O = f . X as Ordinal by A17;

f . X in rng f by A13, A16, FUNCT_1:def 3;

then f . X in sup (rng f) by A17, ORDINAL2:19;

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 & P

the_rank_of O = O by CLASSES1:73;

hence Y c= Rank O2 by A18, A20; :: thesis: P

thus P

A21: ( S

O2 c= O ) ) from ORDINAL1:sch 1(A15);

take O2 ; :: thesis: S

thus S

for x, y1, y2 being set st S

y1 = y2

proof

ex f being Function st
let n be Nat; :: thesis: for x, y1, y2 being set st S_{1}[n,x,y1] & S_{1}[n,x,y2] holds

y1 = y2

let x, y1, y2 be set ; :: thesis: ( S_{1}[n,x,y1] & S_{1}[n,x,y2] implies y1 = y2 )

assume that

A23: S_{1}[n,x,y1]
and

A24: S_{1}[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 (the_rank_of x) holds

ex Y being set st

( Y c= Rank O2 & P_{1}[n,X,Y] ) ) & ( for O being Ordinal st ( for X being set

for n being Nat st X c= Rank (the_rank_of x) holds

ex Y being set st

( Y c= Rank O & P_{1}[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 (the_rank_of x) holds

ex Y being set st

( Y c= Rank O1 & P_{1}[n,X,Y] ) ) & ( for O being Ordinal st ( for X being set

for n being Nat st X c= Rank (the_rank_of x) holds

ex Y being set st

( Y c= Rank O & P_{1}[n,X,Y] ) ) holds

O1 c= O ) ) by A23;

( O1 c= O2 & O2 c= O1 ) by A28, A26;

hence y1 = y2 by A27, A25, XBOOLE_0:def 10; :: thesis: verum

end;y1 = y2

let x, y1, y2 be set ; :: thesis: ( S

assume that

A23: S

A24: S

consider O2 being Ordinal such that

A25: O2 = y2 and

A26: ( ( for X being set

for n being Nat st X c= Rank (the_rank_of x) holds

ex Y being set st

( Y c= Rank O2 & P

for n being Nat st X c= Rank (the_rank_of x) holds

ex Y being set st

( Y c= Rank O & P

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 (the_rank_of x) holds

ex Y being set st

( Y c= Rank O1 & P

for n being Nat st X c= Rank (the_rank_of x) holds

ex Y being set st

( Y c= Rank O & P

O1 c= O ) ) by A23;

( O1 c= O2 & O2 c= O1 ) by A28, A26;

hence y1 = y2 by A27, A25, XBOOLE_0:def 10; :: thesis: verum

( dom f = NAT & f . 0 = the_rank_of F

proof

then consider g being Function such that
deffunc H_{1}( Nat) -> set = { k where k is Nat : k <= $1 } ;

A29: for p, q being Function

for k being Nat st dom p = H_{1}(k) & dom q = H_{1}(k + 1) & p . 0 = q . 0 & ( for n being Nat st n < k holds

( S_{1}[n,p . n,p . (n + 1)] & S_{1}[n,q . n,q . (n + 1)] ) ) holds

p . k = q . k

( dom p = H_{1}(n) & p . 0 = the_rank_of F_{1}() & ( for k being Nat st k < n holds

S_{1}[k,p . k,p . (k + 1)] ) )

( dom f = NAT & ( for n being Nat ex p being Function st

( dom p = H_{1}(n) & p . 0 = the_rank_of F_{1}() & ( for k being Nat st k < n holds

S_{1}[k,p . k,p . (k + 1)] ) & f . n = p . n ) ) )

A66: dom f = NAT and

A67: for n being Nat ex p being Function st

( dom p = H_{1}(n) & p . 0 = the_rank_of F_{1}() & ( for k being Nat st k < n holds

S_{1}[k,p . k,p . (k + 1)] ) & f . n = p . n )
;

take f ; :: thesis: ( dom f = NAT & f . 0 = the_rank_of F_{1}() & ( for n being Nat holds S_{1}[n,f . n,f . (n + 1)] ) )

thus dom f = NAT by A66; :: thesis: ( f . 0 = the_rank_of F_{1}() & ( for n being Nat holds S_{1}[n,f . n,f . (n + 1)] ) )

ex p being Function st

( dom p = H_{1}( 0 ) & p . 0 = the_rank_of F_{1}() & ( for k being Nat st k < 0 holds

S_{1}[k,p . k,p . (k + 1)] ) & f . 0 = p . 0 )
by A67;

hence f . 0 = the_rank_of F_{1}()
; :: thesis: for n being Nat holds S_{1}[n,f . n,f . (n + 1)]

let d be Nat; :: thesis: S_{1}[d,f . d,f . (d + 1)]

consider p being Function such that

A68: dom p = H_{1}(d + 1)
and

A69: p . 0 = the_rank_of F_{1}()
and

A70: for k being Nat st k < d + 1 holds

S_{1}[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 = H_{1}(d)
and

A73: q . 0 = the_rank_of F_{1}()
and

A74: for k being Nat st k < d holds

S_{1}[k,q . k,q . (k + 1)]
and

A75: f . d = q . d by A67;

( dom p = H_{1}(d + 1) & dom q = H_{1}(d) & p . 0 = q . 0 & ( for k being Nat st k < d holds

( S_{1}[k,q . k,q . (k + 1)] & S_{1}[k,p . k,p . (k + 1)] ) ) )

hence S_{1}[d,f . d,f . (d + 1)]
by A70, A71, A75, XREAL_1:29; :: thesis: verum

end;A29: for p, q being Function

for k being Nat st dom p = H

( S

p . k = q . k

proof

A37:
for n being Nat ex p being Function st
let p, q be Function; :: thesis: for k being Nat st dom p = H_{1}(k) & dom q = H_{1}(k + 1) & p . 0 = q . 0 & ( for n being Nat st n < k holds

( S_{1}[n,p . n,p . (n + 1)] & S_{1}[n,q . n,q . (n + 1)] ) ) holds

p . k = q . k

let k be Nat; :: thesis: ( dom p = H_{1}(k) & dom q = H_{1}(k + 1) & p . 0 = q . 0 & ( for n being Nat st n < k holds

( S_{1}[n,p . n,p . (n + 1)] & S_{1}[n,q . n,q . (n + 1)] ) ) implies p . k = q . k )

defpred S_{2}[ Nat] means ( $1 <= k implies p . $1 = q . $1 );

assume that

dom p = H_{1}(k)
and

dom q = H_{1}(k + 1)
and

A30: p . 0 = q . 0 and

A31: for n being Nat st n < k holds

( S_{1}[n,p . n,p . (n + 1)] & S_{1}[n,q . n,q . (n + 1)] )
; :: thesis: p . k = q . k

A32: for n being Nat st S_{2}[n] holds

S_{2}[n + 1]
_{2}[ 0 ]
by A30;

for n being Nat holds S_{2}[n]
from NAT_1:sch 2(A36, A32);

hence p . k = q . k ; :: thesis: verum

end;( S

p . k = q . k

let k be Nat; :: thesis: ( dom p = H

( S

defpred S

assume that

dom p = H

dom q = H

A30: p . 0 = q . 0 and

A31: for n being Nat st n < k holds

( S

A32: for n being Nat st S

S

proof

A36:
S
let n be Nat; :: thesis: ( S_{2}[n] implies S_{2}[n + 1] )

assume A33: ( n <= k implies p . n = q . n ) ; :: thesis: S_{2}[n + 1]

assume n + 1 <= k ; :: thesis: p . (n + 1) = q . (n + 1)

then A34: n < k by NAT_1:13;

then A35: S_{1}[n,p . n,p . (n + 1)]
by A31;

S_{1}[n,p . n,q . (n + 1)]
by A31, A33, A34;

hence p . (n + 1) = q . (n + 1) by A22, A35; :: thesis: verum

end;assume A33: ( n <= k implies p . n = q . n ) ; :: thesis: S

assume n + 1 <= k ; :: thesis: p . (n + 1) = q . (n + 1)

then A34: n < k by NAT_1:13;

then A35: S

S

hence p . (n + 1) = q . (n + 1) by A22, A35; :: thesis: verum

for n being Nat holds S

hence p . k = q . k ; :: thesis: verum

( dom p = H

S

proof

ex f being Function st
defpred S_{2}[ Nat] means ex p being Function st

( dom p = H_{1}($1) & p . 0 = the_rank_of F_{1}() & ( for k being Nat st k < $1 holds

S_{1}[k,p . k,p . (k + 1)] ) );

A38: for n being Nat st S_{2}[n] holds

S_{2}[n + 1]
_{2}[ 0 ]
_{2}[n]
from NAT_1:sch 2(A58, A38); :: thesis: verum

end;( dom p = H

S

A38: for n being Nat st S

S

proof

A58:
S
let n be Nat; :: thesis: ( S_{2}[n] implies S_{2}[n + 1] )

given p being Function such that dom p = H_{1}(n)
and

A39: p . 0 = the_rank_of F_{1}()
and

A40: for k being Nat st k < n holds

S_{1}[k,p . k,p . (k + 1)]
; :: thesis: S_{2}[n + 1]

consider z being set such that

A41: S_{1}[n,p . n,z]
by A2;

defpred S_{3}[ 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 H_{1}(n + 1) holds

ex y being object st S_{3}[x,y]

A49: ( dom q = H_{1}(n + 1) & ( for x being object st x in H_{1}(n + 1) holds

S_{3}[x,q . x] ) )
from CLASSES1:sch 1(A42);

take q ; :: thesis: ( dom q = H_{1}(n + 1) & q . 0 = the_rank_of F_{1}() & ( for k being Nat st k < n + 1 holds

S_{1}[k,q . k,q . (k + 1)] ) )

thus dom q = H_{1}(n + 1)
by A49; :: thesis: ( q . 0 = the_rank_of F_{1}() & ( for k being Nat st k < n + 1 holds

S_{1}[k,q . k,q . (k + 1)] ) )

0 in H_{1}(n + 1)
;

hence q . 0 = the_rank_of F_{1}()
by A39, A49; :: thesis: for k being Nat st k < n + 1 holds

S_{1}[k,q . k,q . (k + 1)]

let k be Nat; :: thesis: ( k < n + 1 implies S_{1}[k,q . k,q . (k + 1)] )

assume A50: k < n + 1 ; :: thesis: S_{1}[k,q . k,q . (k + 1)]

_{1}[k,q . k,q . (k + 1)]
by A51; :: thesis: verum

end;given p being Function such that dom p = H

A39: p . 0 = the_rank_of F

A40: for k being Nat st k < n holds

S

consider z being set such that

A41: S

defpred S

( ( k <= n implies $2 = p . k ) & ( k = n + 1 implies $2 = z ) );

A42: for x being object st x in H

ex y being object st S

proof

consider q being Function such that
let x be object ; :: thesis: ( x in H_{1}(n + 1) implies ex y being object st S_{3}[x,y] )

assume x in H_{1}(n + 1)
; :: thesis: ex y being object st S_{3}[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 S_{3}[x,y] )
_{3}[x,y] )
_{3}[x,y]
by A43, A44, NAT_1:8; :: thesis: verum

end;assume x in H

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 S

proof

( t = n + 1 implies ex y being object st S
assume A45:
t <= n
; :: thesis: ex y being object st S_{3}[x,y]

take p . x ; :: thesis: S_{3}[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 A45, A46;

hence p . x = z by XREAL_1:6; :: thesis: verum

end;take p . x ; :: thesis: S

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 A45, A46;

hence p . x = z by XREAL_1:6; :: thesis: verum

proof

hence
ex y being object st S
assume A47:
t = n + 1
; :: thesis: ex y being object st S_{3}[x,y]

take z ; :: thesis: S_{3}[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 )

end;take z ; :: thesis: S

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

thus
( k = n + 1 implies z = z )
; :: thesis: verum
assume
k <= n
; :: thesis: z = p . k

then n + 1 <= n + 0 by A47, A48;

hence z = p . k by XREAL_1:6; :: thesis: verum

end;then n + 1 <= n + 0 by A47, A48;

hence z = p . k by XREAL_1:6; :: thesis: verum

A49: ( dom q = H

S

take q ; :: thesis: ( dom q = H

S

thus dom q = H

S

0 in H

hence q . 0 = the_rank_of F

S

let k be Nat; :: thesis: ( k < n + 1 implies S

assume A50: k < n + 1 ; :: thesis: S

A51: now :: thesis: ( k <> n implies S_{1}[k,q . k,q . (k + 1)] )

A52:
k + 1 <= n + 1
by A50, NAT_1:13;

assume k <> n ; :: thesis: S_{1}[k,q . k,q . (k + 1)]

then k + 1 <> n + 1 ;

then A53: k + 1 <= n by A52, NAT_1:8;

then A54: k < n by NAT_1:13;

k + 1 in H_{1}(n + 1)
by A52;

then A55: q . (k + 1) = p . (k + 1) by A49, A53;

k in H_{1}(n + 1)
by A50;

then p . k = q . k by A49, A54;

hence S_{1}[k,q . k,q . (k + 1)]
by A40, A55, A54; :: thesis: verum

end;assume k <> n ; :: thesis: S

then k + 1 <> n + 1 ;

then A53: k + 1 <= n by A52, NAT_1:8;

then A54: k < n by NAT_1:13;

k + 1 in H

then A55: q . (k + 1) = p . (k + 1) by A49, A53;

k in H

then p . k = q . k by A49, A54;

hence S

now :: thesis: ( k = n implies S_{1}[k,q . k,q . (k + 1)] )

hence
Sassume A56:
k = n
; :: thesis: S_{1}[k,q . k,q . (k + 1)]

then k <= n + 1 by NAT_1:11;

then k in H_{1}(n + 1)
;

then A57: q . k = p . k by A49, A56;

k + 1 in H_{1}(n + 1)
by A56;

then q . (k + 1) = z by A49, A56;

hence S_{1}[k,q . k,q . (k + 1)]
by A41, A56, A57; :: thesis: verum

end;then k <= n + 1 by NAT_1:11;

then k in H

then A57: q . k = p . k by A49, A56;

k + 1 in H

then q . (k + 1) = z by A49, A56;

hence S

proof

thus
for n being Nat holds S
set s = H_{1}( 0 ) --> (the_rank_of F_{1}());

take H_{1}( 0 ) --> (the_rank_of F_{1}())
; :: thesis: ( dom (H_{1}( 0 ) --> (the_rank_of F_{1}())) = H_{1}( 0 ) & (H_{1}( 0 ) --> (the_rank_of F_{1}())) . 0 = the_rank_of F_{1}() & ( for k being Nat st k < 0 holds

S_{1}[k,(H_{1}( 0 ) --> (the_rank_of F_{1}())) . k,(H_{1}( 0 ) --> (the_rank_of F_{1}())) . (k + 1)] ) )

thus dom (H_{1}( 0 ) --> (the_rank_of F_{1}())) = H_{1}( 0 )
by FUNCOP_1:13; :: thesis: ( (H_{1}( 0 ) --> (the_rank_of F_{1}())) . 0 = the_rank_of F_{1}() & ( for k being Nat st k < 0 holds

S_{1}[k,(H_{1}( 0 ) --> (the_rank_of F_{1}())) . k,(H_{1}( 0 ) --> (the_rank_of F_{1}())) . (k + 1)] ) )

0 in H_{1}( 0 )
;

hence (H_{1}( 0 ) --> (the_rank_of F_{1}())) . 0 = the_rank_of F_{1}()
by FUNCOP_1:7; :: thesis: for k being Nat st k < 0 holds

S_{1}[k,(H_{1}( 0 ) --> (the_rank_of F_{1}())) . k,(H_{1}( 0 ) --> (the_rank_of F_{1}())) . (k + 1)]

thus for k being Nat st k < 0 holds

S_{1}[k,(H_{1}( 0 ) --> (the_rank_of F_{1}())) . k,(H_{1}( 0 ) --> (the_rank_of F_{1}())) . (k + 1)]
; :: thesis: verum

end;take H

S

thus dom (H

S

0 in H

hence (H

S

thus for k being Nat st k < 0 holds

S

( dom f = NAT & ( for n being Nat ex p being Function st

( dom p = H

S

proof

then consider f being Function such that
defpred S_{2}[ object , object ] means for n being Nat st n = $1 holds

ex p being Function st

( dom p = H_{1}(n) & p . 0 = the_rank_of F_{1}() & ( for k being Nat st k < n holds

S_{1}[k,p . k,p . (k + 1)] ) & $2 = p . n );

A59: for x being object st x in NAT holds

ex y being object st S_{2}[x,y]

A62: ( dom f = NAT & ( for x being object st x in NAT holds

S_{2}[x,f . x] ) )
from CLASSES1:sch 1(A59);

take f ; :: thesis: ( dom f = NAT & ( for n being Nat ex p being Function st

( dom p = H_{1}(n) & p . 0 = the_rank_of F_{1}() & ( for k being Nat st k < n holds

S_{1}[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 = H_{1}(n) & p . 0 = the_rank_of F_{1}() & ( for k being Nat st k < n holds

S_{1}[k,p . k,p . (k + 1)] ) & f . n = p . n )

let n be Nat; :: thesis: ex p being Function st

( dom p = H_{1}(n) & p . 0 = the_rank_of F_{1}() & ( for k being Nat st k < n holds

S_{1}[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 = H_{1}(n) & p . 0 = the_rank_of F_{1}() )
and

A64: for k being Nat st k < n holds

S_{1}[k,p . k,p . (k + 1)]
and

A65: f . n = p . n by A62;

take p ; :: thesis: ( dom p = H_{1}(n) & p . 0 = the_rank_of F_{1}() & ( for k being Nat st k < n holds

S_{1}[k,p . k,p . (k + 1)] ) & f . n = p . n )

thus ( dom p = H_{1}(n) & p . 0 = the_rank_of F_{1}() )
by A63; :: thesis: ( ( for k being Nat st k < n holds

S_{1}[k,p . k,p . (k + 1)] ) & f . n = p . n )

thus for k being Nat st k < n holds

S_{1}[k,p . k,p . (k + 1)]
by A64; :: thesis: f . n = p . n

thus f . n = p . n by A65; :: thesis: verum

end;ex p being Function st

( dom p = H

S

A59: for x being object st x in NAT holds

ex y being object st S

proof

consider f being Function such that
let x be object ; :: thesis: ( x in NAT implies ex y being object st S_{2}[x,y] )

assume x in NAT ; :: thesis: ex y being object st S_{2}[x,y]

then reconsider n = x as Nat ;

consider p being Function such that

A60: ( dom p = H_{1}(n) & p . 0 = the_rank_of F_{1}() & ( for k being Nat st k < n holds

S_{1}[k,p . k,p . (k + 1)] ) )
by A37;

take p . n ; :: thesis: S_{2}[x,p . n]

let k be Nat; :: thesis: ( k = x implies ex p being Function st

( dom p = H_{1}(k) & p . 0 = the_rank_of F_{1}() & ( for k being Nat st k < k holds

S_{1}[k,p . k,p . (k + 1)] ) & p . n = p . k ) )

assume A61: k = x ; :: thesis: ex p being Function st

( dom p = H_{1}(k) & p . 0 = the_rank_of F_{1}() & ( for k being Nat st k < k holds

S_{1}[k,p . k,p . (k + 1)] ) & p . n = p . k )

take p ; :: thesis: ( dom p = H_{1}(k) & p . 0 = the_rank_of F_{1}() & ( for k being Nat st k < k holds

S_{1}[k,p . k,p . (k + 1)] ) & p . n = p . k )

thus ( dom p = H_{1}(k) & p . 0 = the_rank_of F_{1}() & ( for k being Nat st k < k holds

S_{1}[k,p . k,p . (k + 1)] ) & p . n = p . k )
by A60, A61; :: thesis: verum

end;assume x in NAT ; :: thesis: ex y being object st S

then reconsider n = x as Nat ;

consider p being Function such that

A60: ( dom p = H

S

take p . n ; :: thesis: S

let k be Nat; :: thesis: ( k = x implies ex p being Function st

( dom p = H

S

assume A61: k = x ; :: thesis: ex p being Function st

( dom p = H

S

take p ; :: thesis: ( dom p = H

S

thus ( dom p = H

S

A62: ( dom f = NAT & ( for x being object st x in NAT holds

S

take f ; :: thesis: ( dom f = NAT & ( for n being Nat ex p being Function st

( dom p = H

S

thus dom f = NAT by A62; :: thesis: for n being Nat ex p being Function st

( dom p = H

S

let n be Nat; :: thesis: ex p being Function st

( dom p = H

S

n in NAT by ORDINAL1:def 12;

then consider p being Function such that

A63: ( dom p = H

A64: for k being Nat st k < n holds

S

A65: f . n = p . n by A62;

take p ; :: thesis: ( dom p = H

S

thus ( dom p = H

S

thus for k being Nat st k < n holds

S

thus f . n = p . n by A65; :: thesis: verum

A66: dom f = NAT and

A67: for n being Nat ex p being Function st

( dom p = H

S

take f ; :: thesis: ( dom f = NAT & f . 0 = the_rank_of F

thus dom f = NAT by A66; :: thesis: ( f . 0 = the_rank_of F

ex p being Function st

( dom p = H

S

hence f . 0 = the_rank_of F

let d be Nat; :: thesis: S

consider p being Function such that

A68: dom p = H

A69: p . 0 = the_rank_of F

A70: for k being Nat st k < d + 1 holds

S

A71: f . (d + 1) = p . (d + 1) by A67;

consider q being Function such that

A72: dom q = H

A73: q . 0 = the_rank_of F

A74: for k being Nat st k < d holds

S

A75: f . d = q . d by A67;

( dom p = H

( S

proof

then
p . d = q . d
by A29;
thus
dom p = H_{1}(d + 1)
by A68; :: thesis: ( dom q = H_{1}(d) & p . 0 = q . 0 & ( for k being Nat st k < d holds

( S_{1}[k,q . k,q . (k + 1)] & S_{1}[k,p . k,p . (k + 1)] ) ) )

thus dom q = H_{1}(d)
by A72; :: thesis: ( p . 0 = q . 0 & ( for k being Nat st k < d holds

( S_{1}[k,q . k,q . (k + 1)] & S_{1}[k,p . k,p . (k + 1)] ) ) )

thus p . 0 = q . 0 by A69, A73; :: thesis: for k being Nat st k < d holds

( S_{1}[k,q . k,q . (k + 1)] & S_{1}[k,p . k,p . (k + 1)] )

let k be Nat; :: thesis: ( k < d implies ( S_{1}[k,q . k,q . (k + 1)] & S_{1}[k,p . k,p . (k + 1)] ) )

assume A76: k < d ; :: thesis: ( S_{1}[k,q . k,q . (k + 1)] & S_{1}[k,p . k,p . (k + 1)] )

hence S_{1}[k,q . k,q . (k + 1)]
by A74; :: thesis: S_{1}[k,p . k,p . (k + 1)]

d <= d + 1 by NAT_1:11;

then k < d + 1 by A76, XXREAL_0:2;

hence S_{1}[k,p . k,p . (k + 1)]
by A70; :: thesis: verum

end;( S

thus dom q = H

( S

thus p . 0 = q . 0 by A69, A73; :: thesis: for k being Nat st k < d holds

( S

let k be Nat; :: thesis: ( k < d implies ( S

assume A76: k < d ; :: thesis: ( S

hence S

d <= d + 1 by NAT_1:11;

then k < d + 1 by A76, XXREAL_0:2;

hence S

hence S

A77: dom g = NAT and

A78: g . 0 = the_rank_of F

A79: for n being Nat holds S

defpred S

( i = $1 `2 & P

( not P

A80: ( [F

set beta = sup (rng g);

A81: for x being object st x in [:(Rank (sup (rng g))),NAT:] holds

ex u being object st S

proof

consider F being Function such that
let x be object ; :: thesis: ( x in [:(Rank (sup (rng g))),NAT:] implies ex u being object st S_{2}[x,u] )

defpred S_{3}[ Ordinal] means ex y being set st

( y c= Rank $1 & P_{1}[x `2 ,x `1 ,y] );

assume x in [:(Rank (sup (rng g))),NAT:] ; :: thesis: ex u being object st S_{2}[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 A82, CLASSES1:66;

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 A86, FUNCT_1:def 3;

reconsider k = k as Nat by A77, A88;

A90: S_{1}[k,alfa,g . (k + 1)]
by A79, A89;

then reconsider O2 = g . (k + 1) as Ordinal ;

reconsider a = a as set by TARSKI:1;

a c= Rank alfa by A87, CLASSES1:65;

then a c= Rank (the_rank_of alfa) by CLASSES1:73;

then ex y being set st

( y c= Rank O2 & P_{1}[x `2 ,x `1 ,y] )
by A90, A85;

then A91: ex O being Ordinal st S_{3}[O]
;

consider O being Ordinal such that

A92: S_{3}[O]
and

A93: for O9 being Ordinal st S_{3}[O9] holds

O c= O9 from ORDINAL1:sch 1(A91);

consider Y being set such that

A94: Y c= Rank O and

A95: P_{1}[b,a,Y]
by A85, A92;

A96: the_rank_of Y c= O by A94, CLASSES1:65;

take u = [Y,(b + 1)]; :: thesis: S_{2}[x,u]

take i = b; :: thesis: ( i = x `2 & P_{1}[x `2 ,x `1 ,u `1 ] & u `2 = i + 1 & ( for y being set holds

( not P_{1}[x `2 ,x `1 ,y] or not the_rank_of y in the_rank_of (u `1) ) ) )

thus i = x `2 by A84; :: thesis: ( P_{1}[x `2 ,x `1 ,u `1 ] & u `2 = i + 1 & ( for y being set holds

( not P_{1}[x `2 ,x `1 ,y] or not the_rank_of y in the_rank_of (u `1) ) ) )

thus P_{1}[x `2 ,x `1 ,u `1 ]
by A85, A95; :: thesis: ( u `2 = i + 1 & ( for y being set holds

( not P_{1}[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 P_{1}[x `2 ,x `1 ,y] or not the_rank_of y in the_rank_of (u `1) )

given y being set such that A97: P_{1}[x `2 ,x `1 ,y]
and

A98: the_rank_of y in the_rank_of (u `1) ; :: thesis: contradiction

A99: y c= Rank (the_rank_of y) 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;defpred S

( y c= Rank $1 & P

assume x in [:(Rank (sup (rng g))),NAT:] ; :: thesis: ex u being object st S

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 A82, CLASSES1:66;

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 A86, FUNCT_1:def 3;

reconsider k = k as Nat by A77, A88;

A90: S

then reconsider O2 = g . (k + 1) as Ordinal ;

reconsider a = a as set by TARSKI:1;

a c= Rank alfa by A87, CLASSES1:65;

then a c= Rank (the_rank_of alfa) by CLASSES1:73;

then ex y being set st

( y c= Rank O2 & P

then A91: ex O being Ordinal st S

consider O being Ordinal such that

A92: S

A93: for O9 being Ordinal st S

O c= O9 from ORDINAL1:sch 1(A91);

consider Y being set such that

A94: Y c= Rank O and

A95: P

A96: the_rank_of Y c= O by A94, CLASSES1:65;

take u = [Y,(b + 1)]; :: thesis: S

take i = b; :: thesis: ( i = x `2 & P

( not P

thus i = x `2 by A84; :: thesis: ( P

( not P

thus P

( not P

thus u `2 = i + 1 ; :: thesis: for y being set holds

( not P

given y being set such that A97: P

A98: the_rank_of y in the_rank_of (u `1) ; :: thesis: contradiction

A99: y c= Rank (the_rank_of y) 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

dom F = [:(Rank (sup (rng g))),NAT:] and

A100: for x being object st x in [:(Rank (sup (rng g))),NAT:] holds

S

deffunc H

consider f being Function such that

A101: dom f = NAT and

A102: f . 0 = F

A103: for n being Nat holds f . (n + 1) = H

defpred S

g . 0 in rng g by A77, FUNCT_1:def 3;

then A104: S

A105: for n being Nat st S

S

proof

A120:
for n being Nat holds S
let n be Nat; :: thesis: ( S_{3}[n] implies S_{3}[n + 1] )

assume A106: the_rank_of (f . n) in sup (rng g) ; :: thesis: S_{3}[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 A106, CLASSES1:66;

then A110: [(f . n),n] in [:(Rank (sup (rng g))),NAT:] by A109, ZFMISC_1:87;

consider m being object such that

A111: m in dom g and

A112: g . m = o1 by A107, FUNCT_1:def 3;

reconsider m = m as Nat by A77, A111;

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 & P_{1}[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 & P_{1}[n,X,Y] ) ) holds

o2 c= o by A79;

the_rank_of (f . n) c= the_rank_of (g . m) by A108, A112, CLASSES1:73;

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: P_{1}[n,f . n,YY]
by A114;

A117: the_rank_of YY c= o2 by A115, CLASSES1:65;

( [(f . n),n] `1 = f . n & [(f . n),n] `2 = n ) ;

then ex i being Nat st

( i = n & P_{1}[n,f . n,(F . [(f . n),n]) `1 ] & (F . [(f . n),n]) `2 = i + 1 & ( for y being set holds

( not P_{1}[n,f . n,y] or not the_rank_of y in the_rank_of ((F . [(f . n),n]) `1) ) ) )
by A100, A110;

then A118: the_rank_of ((F . [(f . n),n]) `1) c= the_rank_of YY by A116, ORDINAL1:16;

g . (m + 1) in rng g by A77, FUNCT_1:def 3;

then A119: o2 in sup (rng g) by A113, ORDINAL2:19;

f . (n + 1) = (F . [(f . n),n]) `1 by A103;

hence S_{3}[n + 1]
by A118, A117, A119, ORDINAL1:12, XBOOLE_1:1; :: thesis: verum

end;assume A106: the_rank_of (f . n) in sup (rng g) ; :: thesis: S

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 A106, CLASSES1:66;

then A110: [(f . n),n] in [:(Rank (sup (rng g))),NAT:] by A109, ZFMISC_1:87;

consider m being object such that

A111: m in dom g and

A112: g . m = o1 by A107, FUNCT_1:def 3;

reconsider m = m as Nat by A77, A111;

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 & P

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 & P

o2 c= o by A79;

the_rank_of (f . n) c= the_rank_of (g . m) by A108, A112, CLASSES1:73;

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: P

A117: the_rank_of YY c= o2 by A115, CLASSES1:65;

( [(f . n),n] `1 = f . n & [(f . n),n] `2 = n ) ;

then ex i being Nat st

( i = n & P

( not P

then A118: the_rank_of ((F . [(f . n),n]) `1) c= the_rank_of YY by A116, ORDINAL1:16;

g . (m + 1) in rng g by A77, FUNCT_1:def 3;

then A119: o2 in sup (rng g) by A113, ORDINAL2:19;

f . (n + 1) = (F . [(f . n),n]) `1 by A103;

hence S

defpred S

A121: for n being Nat st S

S

proof

take
f
; :: thesis: ( dom f = NAT & f . 0 = F
let n be Nat; :: thesis: ( S_{4}[n] implies S_{4}[n + 1] )

assume P_{1}[n,f . n,f . (n + 1)]
; :: thesis: S_{4}[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 & P_{1}[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_{1}[n + 1,f . (n + 1),y] or not the_rank_of y in the_rank_of ((F . [(f . (n + 1)),(n + 1)]) `1) ) ) )
by A100, A122;

hence S_{4}[n + 1]
by A103; :: thesis: verum

end;assume P

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 & P

( not P

hence S

thus dom f = NAT by A101; :: thesis: ( f . 0 = F

thus f . 0 = F

F

then [F

then ex i being Nat st

( i = [F

( not P

then A123: S

thus for n being Nat holds S