:: ORDINAL6 semantic presentation

begin


definition
let X be set ;
attrX is ordinal-membered  means :Def1: :: ORDINAL6:def 1
 ex a being ordinal number st X c= a;
end;

:: deftheorem Def1 defines ordinal-membered ORDINAL6:def_1_:_
 for X being set holds
( X is ordinal-membered iff ex a being ordinal number st X c= a );

registration
cluster ordinal  ->  ordinal-membered for set ;
coherence
 for b1 being set st b1 is ordinal holds
b1 is ordinal-membered
proof
let X be set ; ::_thesis: ( X is ordinal implies X is ordinal-membered )
assume  X is ordinal ; ::_thesis: X is ordinal-membered
hence  ex a being ordinal number st X c= a ; :: according to ORDINAL6:def_1 ::_thesis: verum
end;
let X be set ;
cluster On X ->  ordinal-membered ;
coherence
 On X is ordinal-membered
proof
take  sup X ; :: according to ORDINAL6:def_1 ::_thesis: On X c= sup X
thus  On X c= sup X by ORDINAL2:def_3; ::_thesis: verum
end;
end;

theorem Th1: :: ORDINAL6:1
for X being set holds
( X is ordinal-membered iff for x being set st x in X holds
x is ordinal )
proof
let X be set ; ::_thesis: ( X is ordinal-membered iff for x being set st x in X holds
x is ordinal )
thus  ( X is ordinal-membered implies for x being set st x in X holds
x is ordinal ) ::_thesis: ( ( for x being set st x in X holds
x is ordinal ) implies X is ordinal-membered )
proof
assume  ex a being ordinal number st X c= a ; :: according to ORDINAL6:def_1 ::_thesis: for x being set st x in X holds
x is ordinal
hence  for x being set st x in X holds
x is ordinal ; ::_thesis: verum
end;
assume A1: for x being set st x in X holds
x is ordinal ; ::_thesis: X is ordinal-membered
take a = sup X; :: according to ORDINAL6:def_1 ::_thesis: X c= a
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in a )
assume A2: x in X ; ::_thesis: x in a
then  x is Ordinal by A1;
hence  x in a by A2, ORDINAL2:19; ::_thesis: verum
end;

registration
cluster ordinal-membered for set ;
existence
 ex b1 being set st b1 is ordinal-membered
proof
take  0 ; ::_thesis: 0 is ordinal-membered
take  0 ; :: according to ORDINAL6:def_1 ::_thesis: 0 c= 0
thus  0 c= 0 ; ::_thesis: verum
end;
end;

registration
let X be ordinal-membered set ;
cluster  ->  ordinal for Element of X;
coherence
 for b1 being Element of X holds b1 is ordinal
proof
let a be Element of X; ::_thesis: a is ordinal
percases ( X is empty or not X is empty ) ;
suppose X is empty ; ::_thesis: a is ordinal
hence  a is ordinal ; ::_thesis: verum
end;
suppose not X is empty ; ::_thesis: a is ordinal
hence  a is ordinal by Th1; ::_thesis: verum
end;
end;
end;
end;

theorem Th2: :: ORDINAL6:2
for X being set holds
( X is ordinal-membered iff On X = X )
proof
let X be set ; ::_thesis: ( X is ordinal-membered iff On X = X )
hereby  ::_thesis: ( On X = X implies X is ordinal-membered )
assume A1: X is ordinal-membered ; ::_thesis: On X = X
thus  On X = X ::_thesis: verum
proof
thus  On X c= X by ORDINAL2:7; :: according to XBOOLE_0:def_10 ::_thesis: X c= On X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in On X )
thus  ( not x in X or x in On X ) by A1, ORDINAL1:def_9; ::_thesis: verum
end;
end;
thus  ( On X = X implies X is ordinal-membered ) ; ::_thesis: verum
end;

theorem :: ORDINAL6:3
for X being ordinal-membered set holds X c= sup X
proof
let X be ordinal-membered set ; ::_thesis: X c= sup X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in sup X )
thus  ( not x in X or x in sup X ) by ORDINAL2:19; ::_thesis: verum
end;

theorem Th4: :: ORDINAL6:4
for a, b being ordinal number holds
( a c= b iff b nin a )
proof
let a, b be ordinal number ; ::_thesis: ( a c= b iff b nin a )
 ( a c= b & b in a implies b in b ) ;
hence  ( a c= b iff b nin a ) by ORDINAL1:16; ::_thesis: verum
end;

theorem :: ORDINAL6:5
for a, b being ordinal number
for x being set holds
( x in a \ b iff ( b c= x & x in a ) )
proof
let a, b be ordinal number ; ::_thesis: for x being set holds
( x in a \ b iff ( b c= x & x in a ) )
let x be set ; ::_thesis: ( x in a \ b iff ( b c= x & x in a ) )
 ( x in a \ b iff ( x nin b & x in a ) ) by XBOOLE_0:def_5;
hence  ( x in a \ b iff ( b c= x & x in a ) ) by Th4; ::_thesis: verum
end;

registration
let a, b be ordinal number ;
clustera \ b ->  ordinal-membered ;
coherence
 a \ b is ordinal-membered
proof
take  a ; :: according to ORDINAL6:def_1 ::_thesis: a \ b c= a
thus  a \ b c= a ; ::_thesis: verum
end;
end;

theorem Th6: :: ORDINAL6:6
for X, Y being set
for f being Function st f is_isomorphism_of RelIncl X, RelIncl Y holds
for x, y being set st x in X & y in X holds
( x c= y iff f . x c= f . y )
proof
let X, Y be set ; ::_thesis: for f being Function st f is_isomorphism_of RelIncl X, RelIncl Y holds
for x, y being set st x in X & y in X holds
( x c= y iff f . x c= f . y )
let f be Function; ::_thesis: ( f is_isomorphism_of RelIncl X, RelIncl Y implies for x, y being set st x in X & y in X holds
( x c= y iff f . x c= f . y ) )
assume A1: f is_isomorphism_of RelIncl X, RelIncl Y ; ::_thesis: for x, y being set st x in X & y in X holds
( x c= y iff f . x c= f . y )
let x, y be set ; ::_thesis: ( x in X & y in X implies ( x c= y iff f . x c= f . y ) )
assume A2: ( x in X & y in X ) ; ::_thesis: ( x c= y iff f . x c= f . y )
A3: ( field (RelIncl X) = X & field (RelIncl Y) = Y ) by WELLORD2:def_1;
then  ( dom f = X & rng f = Y ) by A1, WELLORD1:def_7;
then A4: ( f . x in Y & f . y in Y ) by A2, FUNCT_1:def_3;
 ( x c= y iff [x,y] in RelIncl X ) by A2, WELLORD2:def_1;
then  ( x c= y iff [(f . x),(f . y)] in RelIncl Y ) by A1, A2, A3, WELLORD1:def_7;
hence  ( x c= y iff f . x c= f . y ) by A4, WELLORD2:def_1; ::_thesis: verum
end;

theorem :: ORDINAL6:7
for X, Y being ordinal-membered set
for f being Function st f is_isomorphism_of RelIncl X, RelIncl Y holds
for x, y being set st x in X & y in X holds
( x in y iff f . x in f . y )
proof
let X, Y be ordinal-membered set ; ::_thesis: for f being Function st f is_isomorphism_of RelIncl X, RelIncl Y holds
for x, y being set st x in X & y in X holds
( x in y iff f . x in f . y )
let f be Function; ::_thesis: ( f is_isomorphism_of RelIncl X, RelIncl Y implies for x, y being set st x in X & y in X holds
( x in y iff f . x in f . y ) )
assume A1: f is_isomorphism_of RelIncl X, RelIncl Y ; ::_thesis: for x, y being set st x in X & y in X holds
( x in y iff f . x in f . y )
let x, y be set ; ::_thesis: ( x in X & y in X implies ( x in y iff f . x in f . y ) )
assume A2: ( x in X & y in X ) ; ::_thesis: ( x in y iff f . x in f . y )
 ( field (RelIncl X) = X & field (RelIncl Y) = Y ) by WELLORD2:def_1;
then  ( dom f = X & rng f = Y ) by A1, WELLORD1:def_7;
then  ( f . x in Y & f . y in Y ) by A2, FUNCT_1:def_3;
then reconsider a = f . x, b = f . y, x = x, y = y as Ordinal by A2;
 ( y c= x iff b c= a ) by A1, A2, Th6;
hence  ( x in y iff f . x in f . y ) by Th4; ::_thesis: verum
end;

theorem Th8: :: ORDINAL6:8
for x, y, X being set st [x,y] in RelIncl X holds
x c= y
proof
let x, y, X be set ; ::_thesis: ( [x,y] in RelIncl X implies x c= y )
assume A1: [x,y] in RelIncl X ; ::_thesis: x c= y
 field (RelIncl X) = X by WELLORD2:def_1;
then  ( x in X & y in X ) by A1, RELAT_1:15;
hence  x c= y by A1, WELLORD2:def_1; ::_thesis: verum
end;

theorem Th9: :: ORDINAL6:9
for f1, f2 being T-Sequence holds f1 c= f1 ^ f2
proof
let f1, f2 be T-Sequence; ::_thesis: f1 c= f1 ^ f2
 dom (f1 ^ f2) = (dom f1) +^ (dom f2) by ORDINAL4:def_1;
then A1: dom f1 c= dom (f1 ^ f2) by ORDINAL3:24;
 for x being set st x in dom f1 holds
f1 . x = (f1 ^ f2) . x by ORDINAL4:def_1;
hence  f1 c= f1 ^ f2 by A1, GRFUNC_1:2; ::_thesis: verum
end;

theorem Th10: :: ORDINAL6:10
for f1, f2 being T-Sequence holds rng (f1 ^ f2) = (rng f1) \/ (rng f2)
proof
let f1, f2 be T-Sequence; ::_thesis: rng (f1 ^ f2) = (rng f1) \/ (rng f2)
set f = f1 ^ f2;
set A1 = rng f1;
set A2 = rng f2;
A1: dom (f1 ^ f2) = (dom f1) +^ (dom f2) by ORDINAL4:def_1;
thus  rng (f1 ^ f2) c= (rng f1) \/ (rng f2) :: according to XBOOLE_0:def_10 ::_thesis: (rng f1) \/ (rng f2) c= rng (f1 ^ f2)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (f1 ^ f2) or y in (rng f1) \/ (rng f2) )
assume  y in rng (f1 ^ f2) ; ::_thesis: y in (rng f1) \/ (rng f2)
then consider x being set  such that
A2: x in dom (f1 ^ f2) and
A3: y = (f1 ^ f2) . x by FUNCT_1:def_3;
reconsider x = x as Ordinal by A2;
percases ( x in dom f1 or not x in dom f1 ) ;
supposeA4: x in dom f1 ; ::_thesis: y in (rng f1) \/ (rng f2)
then A5: f1 . x in rng f1 by FUNCT_1:def_3;
 y = f1 . x by A3, A4, ORDINAL4:def_1;
hence  y in (rng f1) \/ (rng f2) by A5, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose not x in dom f1 ; ::_thesis: y in (rng f1) \/ (rng f2)
then  dom f1 c= x by ORDINAL1:16;
then A6: (dom f1) +^ (x -^ (dom f1)) = x by ORDINAL3:def_5;
then A7: x -^ (dom f1) in dom f2 by A1, A2, ORDINAL3:22;
then  y = f2 . (x -^ (dom f1)) by A3, A6, ORDINAL4:def_1;
then  y in rng f2 by A7, FUNCT_1:def_3;
hence  y in (rng f1) \/ (rng f2) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (rng f1) \/ (rng f2) or x in rng (f1 ^ f2) )
assume A8: x in (rng f1) \/ (rng f2) ; ::_thesis: x in rng (f1 ^ f2)
A9: dom f1 c= (dom f1) +^ (dom f2) by ORDINAL3:24;
percases ( x in rng f1 or x in rng f2 ) by A8, XBOOLE_0:def_3;
suppose x in rng f1 ; ::_thesis: x in rng (f1 ^ f2)
then consider z being set  such that
A10: ( z in dom f1 & x = f1 . z ) by FUNCT_1:def_3;
 x = (f1 ^ f2) . z by A10, ORDINAL4:def_1;
hence  x in rng (f1 ^ f2) by A1, A9, A10, FUNCT_1:def_3; ::_thesis: verum
end;
suppose x in rng f2 ; ::_thesis: x in rng (f1 ^ f2)
then consider z being set  such that
A11: ( z in dom f2 & x = f2 . z ) by FUNCT_1:def_3;
reconsider z = z as Ordinal by A11;
A12: (dom f1) +^ z in dom (f1 ^ f2) by A1, A11, ORDINAL3:17;
 x = (f1 ^ f2) . ((dom f1) +^ z) by A11, ORDINAL4:def_1;
hence  x in rng (f1 ^ f2) by A12, FUNCT_1:def_3; ::_thesis: verum
end;
end;
end;

theorem Th11: :: ORDINAL6:11
for a, b being ordinal number holds
( a c= b iff epsilon_ a c= epsilon_ b )
proof
let a, b be ordinal number ; ::_thesis: ( a c= b iff epsilon_ a c= epsilon_ b )
hereby  ::_thesis: ( epsilon_ a c= epsilon_ b implies a c= b )
assume  a c= b ; ::_thesis: epsilon_ a c= epsilon_ b
then  ( a = b or a c< b ) by XBOOLE_0:def_8;
then  ( a = b or epsilon_ a in epsilon_ b ) by ORDINAL1:11, ORDINAL5:44;
hence  epsilon_ a c= epsilon_ b by ORDINAL1:def_2; ::_thesis: verum
end;
assume A1: epsilon_ a c= epsilon_ b ; ::_thesis: a c= b
assume  a c/= b ; ::_thesis: contradiction
then  epsilon_ b in epsilon_ a by ORDINAL1:16, ORDINAL5:44;
then  epsilon_ b in epsilon_ b by A1;
hence  contradiction ; ::_thesis: verum
end;

theorem Th12: :: ORDINAL6:12
for a, b being ordinal number holds
( a in b iff epsilon_ a in epsilon_ b )
proof
let a, b be ordinal number ; ::_thesis: ( a in b iff epsilon_ a in epsilon_ b )
 ( b c/= a iff epsilon_ b c/= epsilon_ a ) by Th11;
hence  ( a in b iff epsilon_ a in epsilon_ b ) by Th4; ::_thesis: verum
end;

registration
let X be ordinal-membered set ;
cluster union X ->  ordinal ;
coherence
 union X is ordinal
proof
 ex a being ordinal number st X c= a by Def1;
hence  union X is ordinal by ORDINAL3:4; ::_thesis: verum
end;
end;

registration
let f be Ordinal-yielding Function;
cluster rng f ->  ordinal-membered ;
coherence
 rng f is ordinal-membered
proof
thus  ex a being ordinal number st rng f c= a by ORDINAL2:def_4; :: according to ORDINAL6:def_1 ::_thesis: verum
end;
end;

registration
let a be ordinal number ;
cluster id a ->  T-Sequence-like Ordinal-yielding ;
coherence
 ( id a is T-Sequence-like & id a is Ordinal-yielding )
proof
 ( dom (id a) = a & rng (id a) = a ) ;
hence  ( id a is T-Sequence-like & id a is Ordinal-yielding ) by ORDINAL1:def_7, ORDINAL2:def_4; ::_thesis: verum
end;
end;

registration
let a be ordinal number ;
cluster id a ->  increasing for Ordinal-Sequence;
coherence
 for b1 being Ordinal-Sequence st b1 = id a holds
b1 is increasing
proof
let f be Ordinal-Sequence; ::_thesis: ( f = id a implies f is increasing )
assume A1: f = id a ; ::_thesis: f is increasing
let b be ordinal number ; :: according to ORDINAL2:def_12 ::_thesis: for b1 being set holds
( not b in b1 or not b1 in dom f or f . b in f . b1 )
let c be ordinal number ; ::_thesis: ( not b in c or not c in dom f or f . b in f . c )
assume A2: ( b in c & c in dom f ) ; ::_thesis: f . b in f . c
then  ( b in dom f & dom f = a ) by A1, ORDINAL1:10, RELAT_1:45;
then  ( f . b = b & f . c = c ) by A1, A2, FUNCT_1:18;
hence  f . b in f . c by A2; ::_thesis: verum
end;
end;

registration
let a be ordinal number ;
cluster id a ->  continuous for Ordinal-Sequence;
coherence
 for b1 being Ordinal-Sequence st b1 = id a holds
b1 is continuous
proof
let f be Ordinal-Sequence; ::_thesis: ( f = id a implies f is continuous )
assume A1: f = id a ; ::_thesis: f is continuous
let b be ordinal number ; :: according to ORDINAL2:def_13 ::_thesis: for b1 being set holds
( not b in dom f or b = {} or not b is limit_ordinal or not b1 = f . b or b1 is_limes_of f | b )
let c be ordinal number ; ::_thesis: ( not b in dom f or b = {} or not b is limit_ordinal or not c = f . b or c is_limes_of f | b )
assume A2: ( b in dom f & b <> {} & b is limit_ordinal & c = f . b ) ; ::_thesis: c is_limes_of f | b
set g = f | b;
A3: ( dom f = a & dom (id b) = b ) by A1, RELAT_1:45;
then A4: c = b by A1, A2, FUNCT_1:18;
 b c= a by A2, A3, ORDINAL1:def_2;
then A5: f | b = id b by A1, FUNCT_3:1;
percases ( c = {} or c <> {} ) ;
:: according to ORDINAL2:def_9
case c = {} ; ::_thesis: ex b1 being set st
( b1 in dom (f | b) & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom (f | b) or (f | b) . b2 = {} ) ) )
hence  ex b1 being set st
( b1 in dom (f | b) & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom (f | b) or (f | b) . b2 = {} ) ) ) by A2, A1, A3, FUNCT_1:18; ::_thesis: verum
end;
case c <> {} ; ::_thesis: for b1, b2 being set holds
( not b1 in c or not c in b2 or ex b3 being set st
( b3 in dom (f | b) & ( for b4 being set holds
( not b3 c= b4 or not b4 in dom (f | b) or ( b1 in (f | b) . b4 & (f | b) . b4 in b2 ) ) ) ) )
let B, C be Ordinal; ::_thesis: ( not B in c or not c in C or ex b1 being set st
( b1 in dom (f | b) & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom (f | b) or ( B in (f | b) . b2 & (f | b) . b2 in C ) ) ) ) )
assume A6: ( B in c & c in C ) ; ::_thesis: ex b1 being set st
( b1 in dom (f | b) & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom (f | b) or ( B in (f | b) . b2 & (f | b) . b2 in C ) ) ) )
take D = succ B; ::_thesis: ( D in dom (f | b) & ( for b1 being set holds
( not D c= b1 or not b1 in dom (f | b) or ( B in (f | b) . b1 & (f | b) . b1 in C ) ) ) )
thus  D in dom (f | b) by A2, A3, A4, A5, A6, ORDINAL1:28; ::_thesis: for b1 being set holds
( not D c= b1 or not b1 in dom (f | b) or ( B in (f | b) . b1 & (f | b) . b1 in C ) )
let E be Ordinal; ::_thesis: ( not D c= E or not E in dom (f | b) or ( B in (f | b) . E & (f | b) . E in C ) )
assume A7: ( D c= E & E in dom (f | b) ) ; ::_thesis: ( B in (f | b) . E & (f | b) . E in C )
then  (f | b) . E = E by A3, A5, FUNCT_1:18;
hence  ( B in (f | b) . E & (f | b) . E in C ) by A3, A4, A5, A6, A7, ORDINAL1:10, ORDINAL1:21; ::_thesis: verum
end;
end;
end;
end;

registration
cluster Relation-like Function-like T-Sequence-like non empty Ordinal-yielding increasing continuous for set ;
existence
 ex b1 being Ordinal-Sequence st
( not b1 is empty & b1 is increasing & b1 is continuous )
proof
set A = the ordinal non empty number ;
take  id the ordinal non empty number ; ::_thesis: ( not id the ordinal non empty number is empty & id the ordinal non empty number is increasing & id the ordinal non empty number is continuous )
thus  ( not id the ordinal non empty number is empty & id the ordinal non empty number is increasing & id the ordinal non empty number is continuous ) ; ::_thesis: verum
end;
end;

definition
let f be T-Sequence;
attrf is normal  means :Def2: :: ORDINAL6:def 2
f is increasing continuous Ordinal-Sequence;
end;

:: deftheorem Def2 defines normal ORDINAL6:def_2_:_
 for f being T-Sequence holds
( f is normal iff f is increasing continuous Ordinal-Sequence );

definition
let f be Ordinal-Sequence;
redefine attr f is normal  means :: ORDINAL6:def 3
( f is increasing & f is continuous );
compatibility
 ( f is normal iff ( f is increasing & f is continuous ) ) by Def2;
end;

:: deftheorem  defines normal ORDINAL6:def_3_:_
 for f being Ordinal-Sequence holds
( f is normal iff ( f is increasing & f is continuous ) );

registration
cluster Relation-like Function-like T-Sequence-like normal  ->  Ordinal-yielding for set ;
coherence
 for b1 being T-Sequence st b1 is normal holds
b1 is Ordinal-yielding by Def2;
cluster Relation-like Function-like T-Sequence-like Ordinal-yielding normal  ->  increasing continuous for set ;
coherence
 for b1 being Ordinal-Sequence st b1 is normal holds
( b1 is increasing & b1 is continuous ) by Def2;
cluster Relation-like Function-like T-Sequence-like Ordinal-yielding increasing continuous  ->  normal for set ;
coherence
 for b1 being Ordinal-Sequence st b1 is increasing & b1 is continuous holds
b1 is normal by Def2;
end;

registration
cluster Relation-like Function-like T-Sequence-like non empty normal for set ;
existence
 ex b1 being T-Sequence st
( not b1 is empty & b1 is normal )
proof
set A = the ordinal non empty number ;
take  id the ordinal non empty number ; ::_thesis: ( not id the ordinal non empty number is empty & id the ordinal non empty number is normal )
thus  ( not id the ordinal non empty number is empty & id the ordinal non empty number is normal ) ; ::_thesis: verum
end;
end;

theorem Th13: :: ORDINAL6:13
for a being ordinal number
for f being Ordinal-Sequence st f is non-decreasing holds
f | a is non-decreasing
proof
let a be ordinal number ; ::_thesis: for f being Ordinal-Sequence st f is non-decreasing holds
f | a is non-decreasing
let f be Ordinal-Sequence; ::_thesis: ( f is non-decreasing implies f | a is non-decreasing )
assume A1: for b, c being ordinal number st b in c & c in dom f holds
f . b c= f . c ; :: according to ORDINAL5:def_2 ::_thesis: f | a is non-decreasing
let b be ordinal number ; :: according to ORDINAL5:def_2 ::_thesis: for b1 being set holds
( not b in b1 or not b1 in dom (f | a) or (f | a) . b c= (f | a) . b1 )
let c be ordinal number ; ::_thesis: ( not b in c or not c in dom (f | a) or (f | a) . b c= (f | a) . c )
assume A2: ( b in c & c in dom (f | a) ) ; ::_thesis: (f | a) . b c= (f | a) . c
then A3: ( c in dom f & c in a ) by RELAT_1:57;
then  ( (f | a) . b = f . b & (f | a) . c = f . c ) by A2, FUNCT_1:49, ORDINAL1:10;
hence  (f | a) . b c= (f | a) . c by A1, A2, A3; ::_thesis: verum
end;

definition
let X be set ;
func ord-type X ->  ordinal number  equals :: ORDINAL6:def 4
 order_type_of (RelIncl (On X));
coherence
 order_type_of (RelIncl (On X)) is ordinal number ;
end;

:: deftheorem  defines ord-type ORDINAL6:def_4_:_
 for X being set holds ord-type X = order_type_of (RelIncl (On X));

definition
let X be ordinal-membered set ;
redefine func ord-type X equals :: ORDINAL6:def 5
 order_type_of (RelIncl X);
compatibility
 for b1 being ordinal number holds
( b1 = ord-type X iff b1 = order_type_of (RelIncl X) ) by Th2;
end;

:: deftheorem  defines ord-type ORDINAL6:def_5_:_
 for X being ordinal-membered set holds ord-type X = order_type_of (RelIncl X);

registration
let X be ordinal-membered set ;
cluster RelIncl X ->  well-ordering ;
coherence
 RelIncl X is well-ordering
proof
 ex a being ordinal number st X c= a by Def1;
hence  RelIncl X is well-ordering by WELLORD2:8; ::_thesis: verum
end;
end;

registration
let E be empty set ;
cluster On E ->  empty ;
coherence
 On E is empty by ORDINAL2:7, XBOOLE_1:3;
end;

registration
let E be empty set ;
cluster order_type_of E ->  empty ;
coherence
 order_type_of E is empty
proof
 RelIncl E = E ;
hence  order_type_of E is empty by ORDERS_1:88; ::_thesis: verum
end;
end;

theorem :: ORDINAL6:14
ord-type {} = 0 ;

theorem :: ORDINAL6:15
for a being ordinal number holds ord-type {a} = 1
proof
let a be ordinal number ; ::_thesis: ord-type {a} = 1
 a in succ a by ORDINAL1:6;
then A1: {a} c= succ a by ZFMISC_1:31;
then  order_type_of (RelIncl {a}) = 1 by CARD_5:37;
hence  ord-type {a} = 1 by A1, ORDINAL3:6; ::_thesis: verum
end;

theorem :: ORDINAL6:16
for a, b being ordinal number st a <> b holds
ord-type {a,b} = 2
proof
let a, b be ordinal number ; ::_thesis: ( a <> b implies ord-type {a,b} = 2 )
assume  a <> b ; ::_thesis: ord-type {a,b} = 2
then A1: card {a,b} = 2 by CARD_2:57;
 ( a c= a \/ b & b c= a \/ b ) by XBOOLE_1:7;
then  ( a in succ (a \/ b) & b in succ (a \/ b) ) by ORDINAL1:22;
then A2: {a,b} c= succ (a \/ b) by ZFMISC_1:32;
then  On {a,b} = {a,b} by ORDINAL3:6;
hence  ord-type {a,b} = 2 by A1, A2, CARD_5:36; ::_thesis: verum
end;

theorem :: ORDINAL6:17
for a being ordinal number holds ord-type a = a by ORDERS_1:88;

definition
let X be set ;
func numbering X ->  Ordinal-Sequence equals :: ORDINAL6:def 6
 canonical_isomorphism_of ((RelIncl (ord-type X)),(RelIncl (On X)));
coherence
 canonical_isomorphism_of ((RelIncl (ord-type X)),(RelIncl (On X))) is Ordinal-Sequence
proof
set R1 = RelIncl (ord-type X);
set R2 = RelIncl (On X);
set f = canonical_isomorphism_of ((RelIncl (ord-type X)),(RelIncl (On X)));
consider a being ordinal number  such that
A1: On X c= a by Def1;
 ex phi being Ordinal-Sequence st
( phi = canonical_isomorphism_of ((RelIncl (ord-type X)),(RelIncl (On X))) & phi is increasing & dom phi = ord-type X & rng phi = On X ) by A1, CARD_5:5;
hence  canonical_isomorphism_of ((RelIncl (ord-type X)),(RelIncl (On X))) is Ordinal-Sequence ; ::_thesis: verum
end;
end;

:: deftheorem  defines numbering ORDINAL6:def_6_:_
 for X being set holds numbering X = canonical_isomorphism_of ((RelIncl (ord-type X)),(RelIncl (On X)));

theorem Th18: :: ORDINAL6:18
for X being set holds
( dom (numbering X) = ord-type X & rng (numbering X) = On X )
proof
let X be set ; ::_thesis: ( dom (numbering X) = ord-type X & rng (numbering X) = On X )
set R1 = RelIncl (ord-type X);
set R2 = RelIncl (On X);
set f = canonical_isomorphism_of ((RelIncl (ord-type X)),(RelIncl (On X)));
consider a being ordinal number  such that
A1: On X c= a by Def1;
 ex phi being Ordinal-Sequence st
( phi = canonical_isomorphism_of ((RelIncl (ord-type X)),(RelIncl (On X))) & phi is increasing & dom phi = ord-type X & rng phi = On X ) by A1, CARD_5:5;
hence  ( dom (numbering X) = ord-type X & rng (numbering X) = On X ) ; ::_thesis: verum
end;

theorem Th19: :: ORDINAL6:19
for X being ordinal-membered set holds rng (numbering X) = X
proof
let X be ordinal-membered set ; ::_thesis: rng (numbering X) = X
thus  rng (numbering X) = On X by Th18
.= X by Th2 ; ::_thesis: verum
end;

theorem :: ORDINAL6:20
for X being set holds card (dom (numbering X)) = card (On X)
proof
let X be set ; ::_thesis: card (dom (numbering X)) = card (On X)
 ( dom (numbering X) = ord-type X & ex a being ordinal number st On X c= a ) by Th18, Def1;
hence  card (dom (numbering X)) = card (On X) by CARD_5:7; ::_thesis: verum
end;

theorem Th21: :: ORDINAL6:21
for X being set holds numbering X is_isomorphism_of RelIncl (ord-type X), RelIncl (On X)
proof
let X be set ; ::_thesis: numbering X is_isomorphism_of RelIncl (ord-type X), RelIncl (On X)
set R1 = RelIncl (ord-type X);
set R2 = RelIncl (On X);
 RelIncl (On X), RelIncl (ord-type X) are_isomorphic by WELLORD2:def_2;
then  RelIncl (ord-type X), RelIncl (On X) are_isomorphic by WELLORD1:40;
hence  numbering X is_isomorphism_of RelIncl (ord-type X), RelIncl (On X) by WELLORD1:def_9; ::_thesis: verum
end;

theorem Th22: :: ORDINAL6:22
for X, x, y being set
for f being Ordinal-Sequence st f = numbering X & x in dom f & y in dom f holds
( x c= y iff f . x c= f . y )
proof
let X, x, y be set ; ::_thesis: for f being Ordinal-Sequence st f = numbering X & x in dom f & y in dom f holds
( x c= y iff f . x c= f . y )
let f be Ordinal-Sequence; ::_thesis: ( f = numbering X & x in dom f & y in dom f implies ( x c= y iff f . x c= f . y ) )
assume A1: ( f = numbering X & x in dom f & y in dom f ) ; ::_thesis: ( x c= y iff f . x c= f . y )
then  ( dom f = ord-type X & f is_isomorphism_of RelIncl (ord-type X), RelIncl (On X) ) by Th18, Th21;
hence  ( x c= y iff f . x c= f . y ) by A1, Th6; ::_thesis: verum
end;

theorem Th23: :: ORDINAL6:23
for X, x, y being set
for f being Ordinal-Sequence st f = numbering X & x in dom f & y in dom f holds
( x in y iff f . x in f . y )
proof
let X, x, y be set ; ::_thesis: for f being Ordinal-Sequence st f = numbering X & x in dom f & y in dom f holds
( x in y iff f . x in f . y )
let f be Ordinal-Sequence; ::_thesis: ( f = numbering X & x in dom f & y in dom f implies ( x in y iff f . x in f . y ) )
assume A1: ( f = numbering X & x in dom f & y in dom f ) ; ::_thesis: ( x in y iff f . x in f . y )
then  ( y c= x iff f . y c= f . x ) by Th22;
hence  ( x in y iff f . x in f . y ) by A1, Th4; ::_thesis: verum
end;

registration
let X be set ;
cluster numbering X ->  increasing ;
coherence
 numbering X is increasing
proof
set R1 = RelIncl (ord-type X);
set R2 = RelIncl (On X);
set f = canonical_isomorphism_of ((RelIncl (ord-type X)),(RelIncl (On X)));
consider a being ordinal number  such that
A1: On X c= a by Def1;
 ex phi being Ordinal-Sequence st
( phi = canonical_isomorphism_of ((RelIncl (ord-type X)),(RelIncl (On X))) & phi is increasing & dom phi = ord-type X & rng phi = On X ) by A1, CARD_5:5;
hence  numbering X is increasing ; ::_thesis: verum
end;
end;

registration
let X, Y be ordinal-membered set ;
clusterX \/ Y ->  ordinal-membered ;
coherence
 X \/ Y is ordinal-membered
proof
consider a being ordinal number  such that
A1: X c= a by Def1;
consider b being ordinal number  such that
A2: Y c= b by Def1;
take  a \/ b ; :: according to ORDINAL6:def_1 ::_thesis: X \/ Y c= a \/ b
thus  X \/ Y c= a \/ b by A1, A2, XBOOLE_1:13; ::_thesis: verum
end;
end;

registration
let X be ordinal-membered set ;
let Y be set ;
clusterX \ Y ->  ordinal-membered ;
coherence
 X \ Y is ordinal-membered
proof
consider a being ordinal number  such that
A1: X c= a by Def1;
take  a ; :: according to ORDINAL6:def_1 ::_thesis: X \ Y c= a
thus  X \ Y c= a by A1, XBOOLE_1:1; ::_thesis: verum
end;
end;

theorem Th24: :: ORDINAL6:24
for X, Y being ordinal-membered set st ( for x, y being set st x in X & y in Y holds
x in y ) holds
(numbering X) ^ (numbering Y) is_isomorphism_of RelIncl ((ord-type X) +^ (ord-type Y)), RelIncl (X \/ Y)
proof
let X, Y be ordinal-membered set ; ::_thesis: ( ( for x, y being set st x in X & y in Y holds
x in y ) implies (numbering X) ^ (numbering Y) is_isomorphism_of RelIncl ((ord-type X) +^ (ord-type Y)), RelIncl (X \/ Y) )
assume A1: for x, y being set st x in X & y in Y holds
x in y ; ::_thesis: (numbering X) ^ (numbering Y) is_isomorphism_of RelIncl ((ord-type X) +^ (ord-type Y)), RelIncl (X \/ Y)
set f = numbering X;
set g = numbering Y;
set a = ord-type X;
set b = ord-type Y;
set R = RelIncl ((ord-type X) +^ (ord-type Y));
set Q = RelIncl (X \/ Y);
set R1 = RelIncl (ord-type X);
set Q1 = RelIncl X;
set R2 = RelIncl (ord-type Y);
set Q2 = RelIncl Y;
A2: dom ((numbering X) ^ (numbering Y)) = (dom (numbering X)) +^ (dom (numbering Y)) by ORDINAL4:def_1;
A3: ( dom (numbering X) = ord-type X & dom (numbering Y) = ord-type Y ) by Th18;
A4: ( rng (numbering X) = X & rng (numbering Y) = Y ) by Th19;
A5: ( numbering X is_isomorphism_of RelIncl (ord-type X), RelIncl (On X) & numbering Y is_isomorphism_of RelIncl (ord-type Y), RelIncl (On Y) ) by Th21;
then A6: ( numbering X is one-to-one & numbering Y is one-to-one ) by WELLORD1:def_7;
thus A7: dom ((numbering X) ^ (numbering Y)) = (dom (numbering X)) +^ (dom (numbering Y)) by ORDINAL4:def_1
.= field (RelIncl ((ord-type X) +^ (ord-type Y))) by A3, WELLORD2:def_1 ; :: according to WELLORD1:def_7 ::_thesis: ( rng ((numbering X) ^ (numbering Y)) = field (RelIncl (X \/ Y)) & (numbering X) ^ (numbering Y) is one-to-one & ( for b1, b2 being set holds
( ( not [b1,b2] in RelIncl ((ord-type X) +^ (ord-type Y)) or ( b1 in field (RelIncl ((ord-type X) +^ (ord-type Y))) & b2 in field (RelIncl ((ord-type X) +^ (ord-type Y))) & [(((numbering X) ^ (numbering Y)) . b1),(((numbering X) ^ (numbering Y)) . b2)] in RelIncl (X \/ Y) ) ) & ( not b1 in field (RelIncl ((ord-type X) +^ (ord-type Y))) or not b2 in field (RelIncl ((ord-type X) +^ (ord-type Y))) or not [(((numbering X) ^ (numbering Y)) . b1),(((numbering X) ^ (numbering Y)) . b2)] in RelIncl (X \/ Y) or [b1,b2] in RelIncl ((ord-type X) +^ (ord-type Y)) ) ) ) )
thus  rng ((numbering X) ^ (numbering Y)) = (rng (numbering X)) \/ (rng (numbering Y)) by Th10
.= field (RelIncl (X \/ Y)) by A4, WELLORD2:def_1 ; ::_thesis: ( (numbering X) ^ (numbering Y) is one-to-one & ( for b1, b2 being set holds
( ( not [b1,b2] in RelIncl ((ord-type X) +^ (ord-type Y)) or ( b1 in field (RelIncl ((ord-type X) +^ (ord-type Y))) & b2 in field (RelIncl ((ord-type X) +^ (ord-type Y))) & [(((numbering X) ^ (numbering Y)) . b1),(((numbering X) ^ (numbering Y)) . b2)] in RelIncl (X \/ Y) ) ) & ( not b1 in field (RelIncl ((ord-type X) +^ (ord-type Y))) or not b2 in field (RelIncl ((ord-type X) +^ (ord-type Y))) or not [(((numbering X) ^ (numbering Y)) . b1),(((numbering X) ^ (numbering Y)) . b2)] in RelIncl (X \/ Y) or [b1,b2] in RelIncl ((ord-type X) +^ (ord-type Y)) ) ) ) )
then A8: rng ((numbering X) ^ (numbering Y)) = X \/ Y by WELLORD2:def_1;
A9: ( On X = X & On Y = Y ) by Th2;
thus  (numbering X) ^ (numbering Y) is one-to-one ::_thesis: for b1, b2 being set holds
( ( not [b1,b2] in RelIncl ((ord-type X) +^ (ord-type Y)) or ( b1 in field (RelIncl ((ord-type X) +^ (ord-type Y))) & b2 in field (RelIncl ((ord-type X) +^ (ord-type Y))) & [(((numbering X) ^ (numbering Y)) . b1),(((numbering X) ^ (numbering Y)) . b2)] in RelIncl (X \/ Y) ) ) & ( not b1 in field (RelIncl ((ord-type X) +^ (ord-type Y))) or not b2 in field (RelIncl ((ord-type X) +^ (ord-type Y))) or not [(((numbering X) ^ (numbering Y)) . b1),(((numbering X) ^ (numbering Y)) . b2)] in RelIncl (X \/ Y) or [b1,b2] in RelIncl ((ord-type X) +^ (ord-type Y)) ) )
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom ((numbering X) ^ (numbering Y)) or not b1 in dom ((numbering X) ^ (numbering Y)) or not ((numbering X) ^ (numbering Y)) . x = ((numbering X) ^ (numbering Y)) . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom ((numbering X) ^ (numbering Y)) or not y in dom ((numbering X) ^ (numbering Y)) or not ((numbering X) ^ (numbering Y)) . x = ((numbering X) ^ (numbering Y)) . y or x = y )
assume A10: ( x in dom ((numbering X) ^ (numbering Y)) & y in dom ((numbering X) ^ (numbering Y)) & ((numbering X) ^ (numbering Y)) . x = ((numbering X) ^ (numbering Y)) . y ) ; ::_thesis: x = y
then reconsider a = x, b = y as Ordinal ;
percases ( ( x in dom (numbering X) & y in dom (numbering X) ) or ( x in dom (numbering X) & dom (numbering X) c= y ) or ( dom (numbering X) c= x & y in dom (numbering X) ) or ( dom (numbering X) c= x & dom (numbering X) c= y ) ) by A10, ORDINAL1:16;
supposeA11: ( x in dom (numbering X) & y in dom (numbering X) ) ; ::_thesis: x = y
then  ( ((numbering X) ^ (numbering Y)) . x = (numbering X) . x & ((numbering X) ^ (numbering Y)) . y = (numbering X) . y ) by ORDINAL4:def_1;
hence  x = y by A6, A10, A11, FUNCT_1:def_4; ::_thesis: verum
end;
supposeA12: ( x in dom (numbering X) & dom (numbering X) c= y ) ; ::_thesis: x = y
then A13: (dom (numbering X)) +^ (b -^ (dom (numbering X))) = y by ORDINAL3:def_5;
then A14: b -^ (dom (numbering X)) in dom (numbering Y) by A2, A10, ORDINAL3:22;
then  ( ((numbering X) ^ (numbering Y)) . x = (numbering X) . x & ((numbering X) ^ (numbering Y)) . y = (numbering Y) . (b -^ (dom (numbering X))) ) by A12, A13, ORDINAL4:def_1;
then  ( (numbering X) . x in X & (numbering X) . x in Y ) by A4, A10, A12, A14, FUNCT_1:def_3;
then  (numbering X) . x in (numbering X) . x by A1;
hence  x = y ; ::_thesis: verum
end;
supposeA15: ( dom (numbering X) c= x & y in dom (numbering X) ) ; ::_thesis: x = y
then A16: (dom (numbering X)) +^ (a -^ (dom (numbering X))) = x by ORDINAL3:def_5;
then A17: a -^ (dom (numbering X)) in dom (numbering Y) by A2, A10, ORDINAL3:22;
then  ( ((numbering X) ^ (numbering Y)) . y = (numbering X) . y & ((numbering X) ^ (numbering Y)) . x = (numbering Y) . (a -^ (dom (numbering X))) ) by A15, A16, ORDINAL4:def_1;
then  ( (numbering X) . y in X & (numbering X) . y in Y ) by A4, A10, A15, A17, FUNCT_1:def_3;
then  (numbering X) . y in (numbering X) . y by A1;
hence  x = y ; ::_thesis: verum
end;
suppose ( dom (numbering X) c= x & dom (numbering X) c= y ) ; ::_thesis: x = y
then A18: ( (dom (numbering X)) +^ (a -^ (dom (numbering X))) = x & (dom (numbering X)) +^ (b -^ (dom (numbering X))) = y ) by ORDINAL3:def_5;
then A19: ( a -^ (dom (numbering X)) in dom (numbering Y) & b -^ (dom (numbering X)) in dom (numbering Y) ) by A2, A10, ORDINAL3:22;
then  ( ((numbering X) ^ (numbering Y)) . y = (numbering Y) . (b -^ (dom (numbering X))) & ((numbering X) ^ (numbering Y)) . x = (numbering Y) . (a -^ (dom (numbering X))) ) by A18, ORDINAL4:def_1;
hence  x = y by A6, A10, A18, A19, FUNCT_1:def_4; ::_thesis: verum
end;
end;
end;
let x, y be set ; ::_thesis: ( ( not [x,y] in RelIncl ((ord-type X) +^ (ord-type Y)) or ( x in field (RelIncl ((ord-type X) +^ (ord-type Y))) & y in field (RelIncl ((ord-type X) +^ (ord-type Y))) & [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl (X \/ Y) ) ) & ( not x in field (RelIncl ((ord-type X) +^ (ord-type Y))) or not y in field (RelIncl ((ord-type X) +^ (ord-type Y))) or not [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl (X \/ Y) or [x,y] in RelIncl ((ord-type X) +^ (ord-type Y)) ) )
A20: field (RelIncl ((ord-type X) +^ (ord-type Y))) = (ord-type X) +^ (ord-type Y) by WELLORD2:def_1;
hereby  ::_thesis: ( not x in field (RelIncl ((ord-type X) +^ (ord-type Y))) or not y in field (RelIncl ((ord-type X) +^ (ord-type Y))) or not [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl (X \/ Y) or [x,y] in RelIncl ((ord-type X) +^ (ord-type Y)) )
assume A21: [x,y] in RelIncl ((ord-type X) +^ (ord-type Y)) ; ::_thesis: ( x in field (RelIncl ((ord-type X) +^ (ord-type Y))) & y in field (RelIncl ((ord-type X) +^ (ord-type Y))) & [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl (X \/ Y) )
hence A22: ( x in field (RelIncl ((ord-type X) +^ (ord-type Y))) & y in field (RelIncl ((ord-type X) +^ (ord-type Y))) ) by RELAT_1:15; ::_thesis: [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl (X \/ Y)
then A23: x c= y by A21, A20, WELLORD2:def_1;
A24: ( ((numbering X) ^ (numbering Y)) . x in X \/ Y & ((numbering X) ^ (numbering Y)) . y in X \/ Y ) by A7, A8, A22, FUNCT_1:def_3;
thus  [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl (X \/ Y) ::_thesis: verum
proof
reconsider x = x, y = y as Ordinal by A20, A22;
percases ( ( x in dom (numbering X) & y in dom (numbering X) ) or ( x in dom (numbering X) & dom (numbering X) c= y ) or ( dom (numbering X) c= x & y in dom (numbering X) ) or ( dom (numbering X) c= x & dom (numbering X) c= y ) ) by ORDINAL1:16;
supposeA25: ( x in dom (numbering X) & y in dom (numbering X) ) ; ::_thesis: [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl (X \/ Y)
then A26: [x,y] in RelIncl (ord-type X) by A3, A23, WELLORD2:def_1;
 ( ((numbering X) ^ (numbering Y)) . x = (numbering X) . x & ((numbering X) ^ (numbering Y)) . y = (numbering X) . y ) by A25, ORDINAL4:def_1;
then A27: [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl X by A9, A5, A26, WELLORD1:def_7;
then  ( ((numbering X) ^ (numbering Y)) . x in field (RelIncl X) & ((numbering X) ^ (numbering Y)) . y in field (RelIncl X) ) by RELAT_1:15;
then  ( ((numbering X) ^ (numbering Y)) . x in X & ((numbering X) ^ (numbering Y)) . y in X ) by WELLORD2:def_1;
then  ((numbering X) ^ (numbering Y)) . x c= ((numbering X) ^ (numbering Y)) . y by A27, WELLORD2:def_1;
hence  [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl (X \/ Y) by A24, WELLORD2:def_1; ::_thesis: verum
end;
supposeA28: ( x in dom (numbering X) & dom (numbering X) c= y ) ; ::_thesis: [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl (X \/ Y)
then A29: (dom (numbering X)) +^ (y -^ (dom (numbering X))) = y by ORDINAL3:def_5;
then A30: y -^ (dom (numbering X)) in dom (numbering Y) by A3, A20, A22, ORDINAL3:22;
then  ( ((numbering X) ^ (numbering Y)) . x = (numbering X) . x & ((numbering X) ^ (numbering Y)) . y = (numbering Y) . (y -^ (dom (numbering X))) ) by A28, A29, ORDINAL4:def_1;
then  ( ((numbering X) ^ (numbering Y)) . x in X & ((numbering X) ^ (numbering Y)) . y in Y ) by A4, A28, A30, FUNCT_1:def_3;
then  ((numbering X) ^ (numbering Y)) . x in ((numbering X) ^ (numbering Y)) . y by A1;
then  ((numbering X) ^ (numbering Y)) . x c= ((numbering X) ^ (numbering Y)) . y by ORDINAL1:def_2;
hence  [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl (X \/ Y) by A24, WELLORD2:def_1; ::_thesis: verum
end;
suppose ( dom (numbering X) c= x & y in dom (numbering X) ) ; ::_thesis: [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl (X \/ Y)
then  y in x ;
then  y in y by A23;
hence  [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl (X \/ Y) ; ::_thesis: verum
end;
suppose ( dom (numbering X) c= x & dom (numbering X) c= y ) ; ::_thesis: [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl (X \/ Y)
then A31: ( (dom (numbering X)) +^ (x -^ (dom (numbering X))) = x & (dom (numbering X)) +^ (y -^ (dom (numbering X))) = y ) by ORDINAL3:def_5;
then A32: ( x -^ (dom (numbering X)) in dom (numbering Y) & y -^ (dom (numbering X)) in dom (numbering Y) ) by A3, A20, A22, ORDINAL3:22;
 x -^ (ord-type X) c= y -^ (ord-type X) by A23, ORDINAL3:59;
then A33: [(x -^ (ord-type X)),(y -^ (ord-type X))] in RelIncl (ord-type Y) by A32, A3, WELLORD2:def_1;
 ( ((numbering X) ^ (numbering Y)) . y = (numbering Y) . (y -^ (dom (numbering X))) & ((numbering X) ^ (numbering Y)) . x = (numbering Y) . (x -^ (dom (numbering X))) ) by A31, A32, ORDINAL4:def_1;
then A34: [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl Y by A9, A3, A5, A33, WELLORD1:def_7;
then  ( ((numbering X) ^ (numbering Y)) . x in field (RelIncl Y) & ((numbering X) ^ (numbering Y)) . y in field (RelIncl Y) ) by RELAT_1:15;
then  ( ((numbering X) ^ (numbering Y)) . x in Y & ((numbering X) ^ (numbering Y)) . y in Y ) by WELLORD2:def_1;
then  ((numbering X) ^ (numbering Y)) . x c= ((numbering X) ^ (numbering Y)) . y by A34, WELLORD2:def_1;
hence  [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl (X \/ Y) by A24, WELLORD2:def_1; ::_thesis: verum
end;
end;
end;
end;
assume A35: ( x in field (RelIncl ((ord-type X) +^ (ord-type Y))) & y in field (RelIncl ((ord-type X) +^ (ord-type Y))) & [(((numbering X) ^ (numbering Y)) . x),(((numbering X) ^ (numbering Y)) . y)] in RelIncl (X \/ Y) ) ; ::_thesis: [x,y] in RelIncl ((ord-type X) +^ (ord-type Y))
then A36: ((numbering X) ^ (numbering Y)) . x c= ((numbering X) ^ (numbering Y)) . y by Th8;
A37: ( field (RelIncl (ord-type X)) = ord-type X & field (RelIncl (ord-type Y)) = ord-type Y ) by WELLORD2:def_1;
reconsider x = x, y = y as Ordinal by A20, A35;
percases ( ( x in dom (numbering X) & y in dom (numbering X) ) or ( x in dom (numbering X) & dom (numbering X) c= y ) or ( dom (numbering X) c= x & y in dom (numbering X) ) or ( dom (numbering X) c= x & dom (numbering X) c= y ) ) by ORDINAL1:16;
supposeA38: ( x in dom (numbering X) & y in dom (numbering X) ) ; ::_thesis: [x,y] in RelIncl ((ord-type X) +^ (ord-type Y))
then A39: ( ((numbering X) ^ (numbering Y)) . x = (numbering X) . x & ((numbering X) ^ (numbering Y)) . y = (numbering X) . y ) by ORDINAL4:def_1;
 ( (numbering X) . x in X & (numbering X) . y in X ) by A4, A38, FUNCT_1:def_3;
then  [((numbering X) . x),((numbering X) . y)] in RelIncl X by A39, A36, WELLORD2:def_1;
then  [x,y] in RelIncl (ord-type X) by A9, A38, A37, A3, A5, WELLORD1:def_7;
then  x c= y by Th8;
hence  [x,y] in RelIncl ((ord-type X) +^ (ord-type Y)) by A20, A35, WELLORD2:def_1; ::_thesis: verum
end;
suppose ( x in dom (numbering X) & dom (numbering X) c= y ) ; ::_thesis: [x,y] in RelIncl ((ord-type X) +^ (ord-type Y))
then  x c= y by ORDINAL1:def_2;
hence  [x,y] in RelIncl ((ord-type X) +^ (ord-type Y)) by A20, A35, WELLORD2:def_1; ::_thesis: verum
end;
supposeA40: ( dom (numbering X) c= x & y in dom (numbering X) ) ; ::_thesis: [x,y] in RelIncl ((ord-type X) +^ (ord-type Y))
then A41: ((numbering X) ^ (numbering Y)) . y = (numbering X) . y by ORDINAL4:def_1;
A42: (numbering X) . y in X by A4, A40, FUNCT_1:def_3;
A43: (dom (numbering X)) +^ (x -^ (dom (numbering X))) = x by A40, ORDINAL3:def_5;
then A44: x -^ (dom (numbering X)) in dom (numbering Y) by A3, A20, A35, ORDINAL3:22;
then A45: ((numbering X) ^ (numbering Y)) . x = (numbering Y) . (x -^ (dom (numbering X))) by A43, ORDINAL4:def_1;
 (numbering Y) . (x -^ (dom (numbering X))) in Y by A4, A44, FUNCT_1:def_3;
then  ((numbering X) ^ (numbering Y)) . y in ((numbering X) ^ (numbering Y)) . x by A41, A42, A45, A1;
then  ((numbering X) ^ (numbering Y)) . y in ((numbering X) ^ (numbering Y)) . y by A36;
hence  [x,y] in RelIncl ((ord-type X) +^ (ord-type Y)) ; ::_thesis: verum
end;
suppose ( dom (numbering X) c= x & dom (numbering X) c= y ) ; ::_thesis: [x,y] in RelIncl ((ord-type X) +^ (ord-type Y))
then A46: ( (dom (numbering X)) +^ (x -^ (dom (numbering X))) = x & (dom (numbering X)) +^ (y -^ (dom (numbering X))) = y ) by ORDINAL3:def_5;
then A47: ( x -^ (dom (numbering X)) in dom (numbering Y) & y -^ (dom (numbering X)) in dom (numbering Y) ) by A3, A20, A35, ORDINAL3:22;
then A48: ( (numbering Y) . (y -^ (dom (numbering X))) in Y & (numbering Y) . (x -^ (dom (numbering X))) in Y ) by A4, FUNCT_1:def_3;
 ( ((numbering X) ^ (numbering Y)) . y = (numbering Y) . (y -^ (dom (numbering X))) & ((numbering X) ^ (numbering Y)) . x = (numbering Y) . (x -^ (dom (numbering X))) ) by A46, A47, ORDINAL4:def_1;
then  [((numbering Y) . (x -^ (dom (numbering X)))),((numbering Y) . (y -^ (dom (numbering X))))] in RelIncl Y by A48, A36, WELLORD2:def_1;
then  [(x -^ (dom (numbering X))),(y -^ (dom (numbering X)))] in RelIncl (ord-type Y) by A9, A37, A3, A5, A47, WELLORD1:def_7;
then  x -^ (dom (numbering X)) c= y -^ (dom (numbering X)) by Th8;
then  x c= y by A46, ORDINAL3:18;
hence  [x,y] in RelIncl ((ord-type X) +^ (ord-type Y)) by A20, A35, WELLORD2:def_1; ::_thesis: verum
end;
end;
end;

theorem Th25: :: ORDINAL6:25
for X, Y being ordinal-membered set st ( for x, y being set st x in X & y in Y holds
x in y ) holds
numbering (X \/ Y) = (numbering X) ^ (numbering Y)
proof
let X, Y be ordinal-membered set ; ::_thesis: ( ( for x, y being set st x in X & y in Y holds
x in y ) implies numbering (X \/ Y) = (numbering X) ^ (numbering Y) )
assume A1: for x, y being set st x in X & y in Y holds
x in y ; ::_thesis: numbering (X \/ Y) = (numbering X) ^ (numbering Y)
set f = numbering X;
set g = numbering Y;
set h = numbering (X \/ Y);
set a = ord-type X;
set b = ord-type Y;
set P = RelIncl ((ord-type X) +^ (ord-type Y));
set Q = RelIncl (X \/ Y);
set R = RelIncl (ord-type (X \/ Y));
A2: ( On (X \/ Y) = X \/ Y & On X = X & On Y = Y ) by Th2;
then A3: numbering (X \/ Y) is_isomorphism_of RelIncl (ord-type (X \/ Y)), RelIncl (X \/ Y) by Th21;
A4: (numbering X) ^ (numbering Y) is_isomorphism_of RelIncl ((ord-type X) +^ (ord-type Y)), RelIncl (X \/ Y) by A1, Th24;
then A5: ( RelIncl ((ord-type X) +^ (ord-type Y)), RelIncl (X \/ Y) are_isomorphic & RelIncl (ord-type (X \/ Y)), RelIncl (X \/ Y) are_isomorphic ) by A3, WELLORD1:def_8;
then  RelIncl (X \/ Y), RelIncl (ord-type (X \/ Y)) are_isomorphic by WELLORD1:40;
then  (ord-type X) +^ (ord-type Y) = ord-type (X \/ Y) by A5, WELLORD1:42, WELLORD2:10;
hence  numbering (X \/ Y) = (numbering X) ^ (numbering Y) by A2, A4, A5, WELLORD1:def_9; ::_thesis: verum
end;

theorem :: ORDINAL6:26
for X, Y being ordinal-membered set st ( for x, y being set st x in X & y in Y holds
x in y ) holds
ord-type (X \/ Y) = (ord-type X) +^ (ord-type Y)
proof
let X, Y be ordinal-membered set ; ::_thesis: ( ( for x, y being set st x in X & y in Y holds
x in y ) implies ord-type (X \/ Y) = (ord-type X) +^ (ord-type Y) )
assume  for x, y being set st x in X & y in Y holds
x in y ; ::_thesis: ord-type (X \/ Y) = (ord-type X) +^ (ord-type Y)
then A1: numbering (X \/ Y) = (numbering X) ^ (numbering Y) by Th25;
thus  ord-type (X \/ Y) = dom (numbering (X \/ Y)) by Th18
.= (dom (numbering X)) +^ (dom (numbering Y)) by A1, ORDINAL4:def_1
.= (ord-type X) +^ (dom (numbering Y)) by Th18
.= (ord-type X) +^ (ord-type Y) by Th18 ; ::_thesis: verum
end;

begin

theorem Th27: :: ORDINAL6:27
for x being set
for f being Function st x is_a_fixpoint_of f holds
x in rng f
proof
let x be set ; ::_thesis: for f being Function st x is_a_fixpoint_of f holds
x in rng f
let f be Function; ::_thesis: ( x is_a_fixpoint_of f implies x in rng f )
assume  ( x in dom f & x = f . x ) ; :: according to ABIAN:def_3 ::_thesis: x in rng f
hence  x in rng f by FUNCT_1:def_3; ::_thesis: verum
end;

definition
let f be Ordinal-Sequence;
func criticals f ->  Ordinal-Sequence equals :: ORDINAL6:def 7
 numbering  {  a where a is Element of dom f : a is_a_fixpoint_of f  }  ;
coherence
 numbering  {  a where a is Element of dom f : a is_a_fixpoint_of f  }  is Ordinal-Sequence ;
end;

:: deftheorem  defines criticals ORDINAL6:def_7_:_
 for f being Ordinal-Sequence holds criticals f = numbering  {  a where a is Element of dom f : a is_a_fixpoint_of f  }  ;

theorem Th28: :: ORDINAL6:28
for f being Ordinal-Sequence holds On  {  a where a is Element of dom f : a is_a_fixpoint_of f  }  =  {  a where a is Element of dom f : a is_a_fixpoint_of f  }
proof
let f be Ordinal-Sequence; ::_thesis: On  {  a where a is Element of dom f : a is_a_fixpoint_of f  }  =  {  a where a is Element of dom f : a is_a_fixpoint_of f  }
set X =  {  a where a is Element of dom f : a is_a_fixpoint_of f  }  ;
now__::_thesis:_for_x_being_set_st_x_in__{__a_where_a_is_Element_of_dom_f_:_a_is_a_fixpoint_of_f__}__holds_
x_is_ordinal
let x be set ; ::_thesis: ( x in  {  a where a is Element of dom f : a is_a_fixpoint_of f  }  implies x is ordinal )
assume  x in  {  a where a is Element of dom f : a is_a_fixpoint_of f  }  ; ::_thesis: x is ordinal
then  ex a being Element of dom f st
( x = a & a is_a_fixpoint_of f ) ;
hence  x is ordinal ; ::_thesis: verum
end;
then   {  a where a is Element of dom f : a is_a_fixpoint_of f  }  is ordinal-membered by Th1;
hence  On  {  a where a is Element of dom f : a is_a_fixpoint_of f  }  =  {  a where a is Element of dom f : a is_a_fixpoint_of f  }  by Th2; ::_thesis: verum
end;

theorem Th29: :: ORDINAL6:29
for x being set
for f being Ordinal-Sequence st x in dom (criticals f) holds
(criticals f) . x is_a_fixpoint_of f
proof
let x be set ; ::_thesis: for f being Ordinal-Sequence st x in dom (criticals f) holds
(criticals f) . x is_a_fixpoint_of f
let f be Ordinal-Sequence; ::_thesis: ( x in dom (criticals f) implies (criticals f) . x is_a_fixpoint_of f )
set a = x;
set X =  {  b where b is Element of dom f : b is_a_fixpoint_of f  }  ;
set g = criticals f;
assume  x in dom (criticals f) ; ::_thesis: (criticals f) . x is_a_fixpoint_of f
then  (criticals f) . x in rng (criticals f) by FUNCT_1:def_3;
then  (criticals f) . x in On  {  b where b is Element of dom f : b is_a_fixpoint_of f  }  by Th18;
then  (criticals f) . x in  {  b where b is Element of dom f : b is_a_fixpoint_of f  }  by Th28;
then  ex b being Element of dom f st
( (criticals f) . x = b & b is_a_fixpoint_of f ) ;
hence  (criticals f) . x is_a_fixpoint_of f ; ::_thesis: verum
end;

theorem Th30: :: ORDINAL6:30
for f being Ordinal-Sequence holds
( rng (criticals f) =  {  a where a is Element of dom f : a is_a_fixpoint_of f  }  & rng (criticals f) c= rng f )
proof
let f be Ordinal-Sequence; ::_thesis: ( rng (criticals f) =  {  a where a is Element of dom f : a is_a_fixpoint_of f  }  & rng (criticals f) c= rng f )
set X =  {  a where a is Element of dom f : a is_a_fixpoint_of f  }  ;
 On  {  a where a is Element of dom f : a is_a_fixpoint_of f  }  =  {  a where a is Element of dom f : a is_a_fixpoint_of f  }  by Th28;
hence A1: rng (criticals f) =  {  a where a is Element of dom f : a is_a_fixpoint_of f  }  by Th18; ::_thesis: rng (criticals f) c= rng f
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (criticals f) or x in rng f )
assume  x in rng (criticals f) ; ::_thesis: x in rng f
then  ex a being Element of dom f st
( x = a & a is_a_fixpoint_of f ) by A1;
hence  x in rng f by Th27; ::_thesis: verum
end;

registration
let f be Ordinal-Sequence;
cluster criticals f ->  increasing ;
coherence
 criticals f is increasing ;
end;

theorem :: ORDINAL6:31
for x being set
for f being Ordinal-Sequence st x in dom (criticals f) holds
x c= (criticals f) . x by ORDINAL4:10;

theorem Th32: :: ORDINAL6:32
for f being Ordinal-Sequence holds dom (criticals f) c= dom f
proof
let f be Ordinal-Sequence; ::_thesis: dom (criticals f) c= dom f
let x be Ordinal; :: according to ORDINAL1:def_5 ::_thesis: ( not x in dom (criticals f) or x in dom f )
set X =  {  a where a is Element of dom f : a is_a_fixpoint_of f  }  ;
assume A1: x in dom (criticals f) ; ::_thesis: x in dom f
then  (criticals f) . x in rng (criticals f) by FUNCT_1:def_3;
then  (criticals f) . x in On  {  a where a is Element of dom f : a is_a_fixpoint_of f  }  by Th18;
then  (criticals f) . x in  {  a where a is Element of dom f : a is_a_fixpoint_of f  }  by Th28;
then consider a being Element of dom f such that
A2: ( (criticals f) . x = a & a is_a_fixpoint_of f ) ;
 ( x c= a & a in dom f & a = f . a ) by A1, A2, ABIAN:def_3, ORDINAL4:10;
hence  x in dom f by ORDINAL1:12; ::_thesis: verum
end;

theorem Th33: :: ORDINAL6:33
for b being ordinal number
for f being Ordinal-Sequence st b is_a_fixpoint_of f holds
ex a being ordinal number st
( a in dom (criticals f) & b = (criticals f) . a )
proof
let b be ordinal number ; ::_thesis: for f being Ordinal-Sequence st b is_a_fixpoint_of f holds
ex a being ordinal number st
( a in dom (criticals f) & b = (criticals f) . a )
let f be Ordinal-Sequence; ::_thesis: ( b is_a_fixpoint_of f implies ex a being ordinal number st
( a in dom (criticals f) & b = (criticals f) . a ) )
set X =  {  a where a is Element of dom f : a is_a_fixpoint_of f  }  ;
assume A1: b is_a_fixpoint_of f ; ::_thesis: ex a being ordinal number st
( a in dom (criticals f) & b = (criticals f) . a )
then  b in dom f by ABIAN:def_3;
then  b in  {  a where a is Element of dom f : a is_a_fixpoint_of f  }  by A1;
then  b in rng (criticals f) by Th30;
then  ex x being set st
( x in dom (criticals f) & b = (criticals f) . x ) by FUNCT_1:def_3;
hence  ex a being ordinal number st
( a in dom (criticals f) & b = (criticals f) . a ) ; ::_thesis: verum
end;

theorem :: ORDINAL6:34
for a, b being ordinal number
for f being Ordinal-Sequence st a in dom (criticals f) & b is_a_fixpoint_of f & (criticals f) . a in b holds
succ a in dom (criticals f)
proof
let a, b be ordinal number ; ::_thesis: for f being Ordinal-Sequence st a in dom (criticals f) & b is_a_fixpoint_of f & (criticals f) . a in b holds
succ a in dom (criticals f)
let f be Ordinal-Sequence; ::_thesis: ( a in dom (criticals f) & b is_a_fixpoint_of f & (criticals f) . a in b implies succ a in dom (criticals f) )
set g = criticals f;
assume that
A1: a in dom (criticals f) and
A2: b is_a_fixpoint_of f and
A3: (criticals f) . a in b ; ::_thesis: succ a in dom (criticals f)
consider c being ordinal number  such that
A4: ( c in dom (criticals f) & b = (criticals f) . c ) by A2, Th33;
 a in c by A1, A3, A4, Th23;
then  succ a c= c by ORDINAL1:21;
hence  succ a in dom (criticals f) by A4, ORDINAL1:12; ::_thesis: verum
end;

theorem :: ORDINAL6:35
for a, b being ordinal number
for f being Ordinal-Sequence st succ a in dom (criticals f) & b is_a_fixpoint_of f & (criticals f) . a in b holds
(criticals f) . (succ a) c= b
proof
let a, b be ordinal number ; ::_thesis: for f being Ordinal-Sequence st succ a in dom (criticals f) & b is_a_fixpoint_of f & (criticals f) . a in b holds
(criticals f) . (succ a) c= b
let f be Ordinal-Sequence; ::_thesis: ( succ a in dom (criticals f) & b is_a_fixpoint_of f & (criticals f) . a in b implies (criticals f) . (succ a) c= b )
set g = criticals f;
set Y =  {  c where c is Element of dom f : c is_a_fixpoint_of f  }  ;
set X = ord-type  {  c where c is Element of dom f : c is_a_fixpoint_of f  }  ;
assume A1: ( succ a in dom (criticals f) & b is_a_fixpoint_of f & (criticals f) . a in b ) ; ::_thesis: (criticals f) . (succ a) c= b
then consider c being ordinal number  such that
A2: ( c in dom (criticals f) & b = (criticals f) . c ) by Th33;
 a in succ a by ORDINAL1:6;
then A3: ( a in dom (criticals f) & (criticals f) . a in (criticals f) . (succ a) ) by A1, ORDINAL1:10, ORDINAL2:def_12;
 On  {  c where c is Element of dom f : c is_a_fixpoint_of f  }  =  {  c where c is Element of dom f : c is_a_fixpoint_of f  }  by Th28;
then A4: criticals f is_isomorphism_of RelIncl (ord-type  {  c where c is Element of dom f : c is_a_fixpoint_of f  }  ), RelIncl  {  c where c is Element of dom f : c is_a_fixpoint_of f  }  by Th21;
A5: dom (criticals f) = ord-type  {  c where c is Element of dom f : c is_a_fixpoint_of f  }  by Th18;
 b c/= (criticals f) . a by A1, Th4;
then  c c/= a by A2, A3, A4, A5, Th6;
then  a in c by Th4;
then  succ a c= c by ORDINAL1:21;
hence  (criticals f) . (succ a) c= b by A2, ORDINAL4:9; ::_thesis: verum
end;

theorem Th36: :: ORDINAL6:36
for X being set
for f being Ordinal-Sequence st f is normal & union X in dom f & not X is empty & ( for x being set st x in X holds
ex y being set st
( x c= y & y in X & y is_a_fixpoint_of f ) ) holds
union X = f . (union X)
proof
let X be set ; ::_thesis: for f being Ordinal-Sequence st f is normal & union X in dom f & not X is empty & ( for x being set st x in X holds
ex y being set st
( x c= y & y in X & y is_a_fixpoint_of f ) ) holds
union X = f . (union X)
let f be Ordinal-Sequence; ::_thesis: ( f is normal & union X in dom f & not X is empty & ( for x being set st x in X holds
ex y being set st
( x c= y & y in X & y is_a_fixpoint_of f ) ) implies union X = f . (union X) )
assume that
A1: f is normal and
A2: ( union X in dom f & not X is empty ) and
A3: for x being set st x in X holds
ex y being set st
( x c= y & y in X & y is_a_fixpoint_of f ) ; ::_thesis: union X = f . (union X)
reconsider l = union X as Ordinal by A2;
percases ( ex a being ordinal number st
( a in X & ( for b being ordinal number st b in X holds
b c= a ) ) or for a being ordinal number holds
( not a in X or ex b being ordinal number st
( b in X & not b c= a ) ) ) ;
suppose ex a being ordinal number st
( a in X & ( for b being ordinal number st b in X holds
b c= a ) ) ; ::_thesis: union X = f . (union X)
then consider a being ordinal number  such that
A4: ( a in X & ( for b being ordinal number st b in X holds
b c= a ) ) ;
now__::_thesis:_for_x_being_set_st_x_in_X_holds_
x_c=_a
let x be set ; ::_thesis: ( x in X implies x c= a )
assume  x in X ; ::_thesis: x c= a
then consider y being set  such that
A5: ( x c= y & y in X & y is_a_fixpoint_of f ) by A3;
 y in dom f by A5, ABIAN:def_3;
then  y c= a by A4, A5;
hence  x c= a by A5, XBOOLE_1:1; ::_thesis: verum
end;
then  ( union X c= a & a c= union X ) by A4, ZFMISC_1:74, ZFMISC_1:76;
then A6: union X = a by XBOOLE_0:def_10;
then consider y being set  such that
A7: ( union X c= y & y in X & y is_a_fixpoint_of f ) by A3, A4;
 ( y in dom f & y = f . y ) by A7, ABIAN:def_3;
then  y c= union X by A6, A7, A4;
then  y = union X by A7, XBOOLE_0:def_10;
hence  union X = f . (union X) by A7, ABIAN:def_3; ::_thesis: verum
end;
supposeA8: for a being ordinal number holds
( not a in X or ex b being ordinal number st
( b in X & not b c= a ) ) ; ::_thesis: union X = f . (union X)
set y0 = the Element of X;
consider x0 being set  such that
A9: ( the Element of X c= x0 & x0 in X & x0 is_a_fixpoint_of f ) by A2, A3;
A10: x0 in dom f by A9, ABIAN:def_3;
then consider b being ordinal number  such that
A11: ( b in X & b c/= x0 ) by A9, A8;
A12: x0 in b by A10, A11, Th4;
now__::_thesis:_for_a_being_ordinal_number_st_a_in_l_holds_
succ_a_in_l
let a be ordinal number ; ::_thesis: ( a in l implies succ a in l )
assume  a in l ; ::_thesis: succ a in l
then consider x being set  such that
A13: ( a in x & x in X ) by TARSKI:def_4;
consider y being set  such that
A14: ( x c= y & y in X & y is_a_fixpoint_of f ) by A3, A13;
A15: y in dom f by A14, ABIAN:def_3;
then consider b being ordinal number  such that
A16: ( b in X & b c/= y ) by A8, A14;
 ( succ a c= y & y in b ) by A13, A14, A15, A16, Th4, ORDINAL1:21;
then  succ a in b by ORDINAL1:12;
hence  succ a in l by A16, TARSKI:def_4; ::_thesis: verum
end;
then reconsider l = l as limit_ordinal non empty Ordinal by A12, A11, ORDINAL1:28, TARSKI:def_4;
thus  union X c= f . (union X) by A2, A1, ORDINAL4:10; :: according to XBOOLE_0:def_10 ::_thesis: f . (union X) c= union X
reconsider g = f | l as increasing Ordinal-Sequence by A1, ORDINAL4:15;
 l c= dom f by A2, ORDINAL1:def_2;
then A17: dom g = l by RELAT_1:62;
then A18: Union g is_limes_of g by ORDINAL5:6;
 f . l is_limes_of g by A1, A2, ORDINAL2:def_13;
then A19: ( f . l = lim g & Union g = lim g ) by A18, ORDINAL2:def_10;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f . (union X) or x in union X )
assume  x in f . (union X) ; ::_thesis: x in union X
then consider z being set  such that
A20: ( z in dom g & x in g . z ) by A19, CARD_5:2;
consider y being set  such that
A21: ( z in y & y in X ) by A17, A20, TARSKI:def_4;
consider t being set  such that
A22: ( y c= t & t in X & t is_a_fixpoint_of f ) by A21, A3;
A23: ( t in dom f & t = f . t ) by A22, ABIAN:def_3;
then reconsider z = z, t = t as Ordinal by A20;
 ( f . z = g . z & z in t ) by A20, A21, A22, FUNCT_1:47;
then  g . z in t by A1, A23, ORDINAL2:def_12;
then  x in t by A20, ORDINAL1:10;
hence  x in union X by A22, TARSKI:def_4; ::_thesis: verum
end;
end;
end;

theorem Th37: :: ORDINAL6:37
for X being set
for f being Ordinal-Sequence st f is normal & union X in dom f & not X is empty & ( for x being set st x in X holds
x is_a_fixpoint_of f ) holds
union X = f . (union X)
proof
let X be set ; ::_thesis: for f being Ordinal-Sequence st f is normal & union X in dom f & not X is empty & ( for x being set st x in X holds
x is_a_fixpoint_of f ) holds
union X = f . (union X)
let f be Ordinal-Sequence; ::_thesis: ( f is normal & union X in dom f & not X is empty & ( for x being set st x in X holds
x is_a_fixpoint_of f ) implies union X = f . (union X) )
assume that
A1: f is normal and
A2: ( union X in dom f & not X is empty ) and
A3: for x being set st x in X holds
x is_a_fixpoint_of f ; ::_thesis: union X = f . (union X)
 for x being set st x in X holds
ex y being set st
( x c= y & y in X & y is_a_fixpoint_of f ) by A3;
hence  union X = f . (union X) by A1, A2, Th36; ::_thesis: verum
end;

theorem Th38: :: ORDINAL6:38
for a being ordinal number
for l being limit_ordinal non empty Ordinal
for f being Ordinal-Sequence st l c= dom (criticals f) & a is_a_fixpoint_of f & ( for x being set st x in l holds
(criticals f) . x in a ) holds
l in dom (criticals f)
proof
let a be ordinal number ; ::_thesis: for l being limit_ordinal non empty Ordinal
for f being Ordinal-Sequence st l c= dom (criticals f) & a is_a_fixpoint_of f & ( for x being set st x in l holds
(criticals f) . x in a ) holds
l in dom (criticals f)
let l be limit_ordinal non empty Ordinal; ::_thesis: for f being Ordinal-Sequence st l c= dom (criticals f) & a is_a_fixpoint_of f & ( for x being set st x in l holds
(criticals f) . x in a ) holds
l in dom (criticals f)
let f be Ordinal-Sequence; ::_thesis: ( l c= dom (criticals f) & a is_a_fixpoint_of f & ( for x being set st x in l holds
(criticals f) . x in a ) implies l in dom (criticals f) )
set g = criticals f;
assume that
A1: l c= dom (criticals f) and
A2: a is_a_fixpoint_of f and
A3: for x being set st x in l holds
(criticals f) . x in a ; ::_thesis: l in dom (criticals f)
consider b being ordinal number  such that
A4: ( b in dom (criticals f) & a = (criticals f) . b ) by A2, Th33;
 l c= b
proof
let x be Ordinal; :: according to ORDINAL1:def_5 ::_thesis: ( not x in l or x in b )
assume  x in l ; ::_thesis: x in b
then  ( x in dom (criticals f) & (criticals f) . x in (criticals f) . b ) by A1, A3, A4;
hence  x in b by A4, Th23; ::_thesis: verum
end;
hence  l in dom (criticals f) by A4, ORDINAL1:12; ::_thesis: verum
end;

theorem Th39: :: ORDINAL6:39
for l being limit_ordinal non empty Ordinal
for f being Ordinal-Sequence st f is normal & l in dom (criticals f) holds
(criticals f) . l = Union ((criticals f) | l)
proof
let l be limit_ordinal non empty Ordinal; ::_thesis: for f being Ordinal-Sequence st f is normal & l in dom (criticals f) holds
(criticals f) . l = Union ((criticals f) | l)
let f be Ordinal-Sequence; ::_thesis: ( f is normal & l in dom (criticals f) implies (criticals f) . l = Union ((criticals f) | l) )
set g = criticals f;
reconsider h = (criticals f) | l as increasing Ordinal-Sequence by ORDINAL4:15;
set X = rng h;
assume A1: ( f is normal & l in dom (criticals f) ) ; ::_thesis: (criticals f) . l = Union ((criticals f) | l)
then  (criticals f) . l is_a_fixpoint_of f by Th29;
then A2: ( (criticals f) . l in dom f & f . ((criticals f) . l) = (criticals f) . l ) by ABIAN:def_3;
A3: l c= dom (criticals f) by A1, ORDINAL1:def_2;
then A4: dom h = l by RELAT_1:62;
A5: for x being set st x in rng h holds
x is_a_fixpoint_of f
proof
let x be set ; ::_thesis: ( x in rng h implies x is_a_fixpoint_of f )
assume  x in rng h ; ::_thesis: x is_a_fixpoint_of f
then consider y being set  such that
A6: ( y in dom h & x = h . y ) by FUNCT_1:def_3;
 ( x = (criticals f) . y & y in dom (criticals f) ) by A3, A4, A6, FUNCT_1:47;
hence  x is_a_fixpoint_of f by Th29; ::_thesis: verum
end;
reconsider u = union (rng h) as Ordinal ;
A7: h <> {} by A4;
now__::_thesis:_for_x_being_set_st_x_in_rng_h_holds_
x_c=_(criticals_f)_._l
let x be set ; ::_thesis: ( x in rng h implies x c= (criticals f) . l )
assume  x in rng h ; ::_thesis: x c= (criticals f) . l
then consider y being set  such that
A8: ( y in dom h & x = h . y ) by FUNCT_1:def_3;
 ( x = (criticals f) . y & y in dom (criticals f) ) by A3, A4, A8, FUNCT_1:47;
then  x in (criticals f) . l by A1, A4, A8, ORDINAL2:def_12;
hence  x c= (criticals f) . l by ORDINAL1:def_2; ::_thesis: verum
end;
then A9: union (rng h) c= (criticals f) . l by ZFMISC_1:76;
then A10: u in dom f by A2, ORDINAL1:12;
 u = f . u by A1, A5, A7, A9, Th37, A2, ORDINAL1:12;
then  u is_a_fixpoint_of f by A10, ABIAN:def_3;
then consider a being ordinal number  such that
A11: ( a in dom (criticals f) & u = (criticals f) . a ) by Th33;
 a = l
proof
thus  a c= l by A1, A11, A9, Th22; :: according to XBOOLE_0:def_10 ::_thesis: l c= a
let x be Ordinal; :: according to ORDINAL1:def_5 ::_thesis: ( not x in l or x in a )
assume A12: x in l ; ::_thesis: x in a
then A13: succ x in l by ORDINAL1:28;
then A14: ( (criticals f) . x = h . x & (criticals f) . (succ x) = h . (succ x) & h . (succ x) in rng h ) by A4, A12, FUNCT_1:47, FUNCT_1:def_3;
 x in succ x by ORDINAL1:6;
then  h . x in h . (succ x) by A4, A13, ORDINAL2:def_12;
then  (criticals f) . x in u by A14, TARSKI:def_4;
then  ( (criticals f) . a c/= (criticals f) . x & x in dom (criticals f) ) by A3, A11, A12, Th4;
then  a c/= x by A11, Th22;
hence  x in a by Th4; ::_thesis: verum
end;
hence  (criticals f) . l = Union ((criticals f) | l) by A11; ::_thesis: verum
end;

registration
let f be normal Ordinal-Sequence;
cluster criticals f ->  continuous ;
coherence
 criticals f is continuous
proof
set g = criticals f;
let a be ordinal number ; :: according to ORDINAL2:def_13 ::_thesis: for b1 being set holds
( not a in dom (criticals f) or a = {} or not a is limit_ordinal or not b1 = (criticals f) . a or b1 is_limes_of (criticals f) | a )
let b be ordinal number ; ::_thesis: ( not a in dom (criticals f) or a = {} or not a is limit_ordinal or not b = (criticals f) . a or b is_limes_of (criticals f) | a )
reconsider h = (criticals f) | a as increasing Ordinal-Sequence by ORDINAL4:15;
assume A1: ( a in dom (criticals f) & a <> {} & a is limit_ordinal & b = (criticals f) . a ) ; ::_thesis: b is_limes_of (criticals f) | a
then A2: b = Union h by Th39;
 a c= dom (criticals f) by A1, ORDINAL1:def_2;
then  dom h = a by RELAT_1:62;
hence  b is_limes_of (criticals f) | a by A1, A2, ORDINAL5:6; ::_thesis: verum
end;
end;

theorem Th40: :: ORDINAL6:40
for f1, f2 being Ordinal-Sequence st f1 c= f2 holds
criticals f1 c= criticals f2
proof
let f1, f2 be Ordinal-Sequence; ::_thesis: ( f1 c= f2 implies criticals f1 c= criticals f2 )
assume A1: f1 c= f2 ; ::_thesis: criticals f1 c= criticals f2
then A2: dom f1 c= dom f2 by GRFUNC_1:2;
set X =  {  a where a is Element of dom f1 : a is_a_fixpoint_of f1  }  ;
set Z =  {  a where a is Element of dom f2 : a is_a_fixpoint_of f2  }  ;
 ( On  {  a where a is Element of dom f1 : a is_a_fixpoint_of f1  }  =  {  a where a is Element of dom f1 : a is_a_fixpoint_of f1  }  & On  {  a where a is Element of dom f2 : a is_a_fixpoint_of f2  }  =  {  a where a is Element of dom f2 : a is_a_fixpoint_of f2  }  ) by Th28;
then reconsider X =  {  a where a is Element of dom f1 : a is_a_fixpoint_of f1  }  , Z =  {  a where a is Element of dom f2 : a is_a_fixpoint_of f2  }  as ordinal-membered set ;
set Y = Z \ X;
A3: now__::_thesis:_for_x,_y_being_set_st_x_in_X_&_y_in_Z_\_X_holds_
x_in_y
let x, y be set ; ::_thesis: ( x in X & y in Z \ X implies x in y )
assume  x in X ; ::_thesis: ( y in Z \ X implies x in y )
then consider a being Element of dom f1 such that
A4: ( x = a & a is_a_fixpoint_of f1 ) ;
assume  y in Z \ X ; ::_thesis: x in y
then A5: ( y in Z & not y in X ) by XBOOLE_0:def_5;
then consider b being Element of dom f2 such that
A6: ( y = b & b is_a_fixpoint_of f2 ) ;
now__::_thesis:_not_b_in_dom_f1
assume A7: b in dom f1 ; ::_thesis: contradiction
then f1 . b = f2 . b by A1, GRFUNC_1:2
.= b by A6, ABIAN:def_3 ;
then  b is_a_fixpoint_of f1 by A7, ABIAN:def_3;
hence  contradiction by A5, A6, A7; ::_thesis: verum
end;
then  ( dom f1 c= b & x in dom f1 ) by A4, Th4, ABIAN:def_3;
hence  x in y by A6; ::_thesis: verum
end;
 X c= Z
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Z )
assume  x in X ; ::_thesis: x in Z
then consider a being Element of dom f1 such that
A8: ( x = a & a is_a_fixpoint_of f1 ) ;
A9: ( a in dom f1 & a = f1 . a ) by A8, ABIAN:def_3;
then  ( a in dom f2 & a = f2 . a ) by A1, A2, GRFUNC_1:2;
then  a is_a_fixpoint_of f2 by ABIAN:def_3;
hence  x in Z by A8, A9, A2; ::_thesis: verum
end;
then  X \/ (Z \ X) = Z by XBOOLE_1:45;
then  criticals f2 = (criticals f1) ^ (numbering (Z \ X)) by A3, Th25;
hence  criticals f1 c= criticals f2 by Th9; ::_thesis: verum
end;

begin


registration
let U be Universe;
cluster Relation-like On U -defined On U -valued Function-like T-Sequence-like non empty V26( On U) V30( On U, On U) Ordinal-yielding normal for Element of bool [:(On U),(On U):];
existence
 ex b1 being Ordinal-Sequence of U st b1 is normal
proof
reconsider F = id (On U) as Ordinal-Sequence of U ;
take  F ; ::_thesis: F is normal
thus  F is normal ; ::_thesis: verum
end;
end;

definition
let U be Universe;
let a be ordinal number ;
mode Ordinal-Sequence of a,U is Function of a,(On U);
end;

registration
let U be Universe;
let a be ordinal number ;
cluster Function-like V30(a, On U)  ->  T-Sequence-like Ordinal-yielding for Element of bool [:a,(On U):];
coherence
 for b1 being Ordinal-Sequence of a,U holds
( b1 is T-Sequence-like & b1 is Ordinal-yielding )
proof
let f be Ordinal-Sequence of a,U; ::_thesis: ( f is T-Sequence-like & f is Ordinal-yielding )
thus  dom f is ordinal by FUNCT_2:def_1; :: according to ORDINAL1:def_7 ::_thesis: f is Ordinal-yielding
take  On U ; :: according to ORDINAL2:def_4 ::_thesis: rng f c= On U
thus  rng f c= On U by RELAT_1:def_19; ::_thesis: verum
end;
end;

definition
let U be Universe;
let a be ordinal number ;
let f be Ordinal-Sequence of a,U;
let x be set ;
:: original: .
redefine funcf . x ->  Ordinal of U;
coherence
 f . x is Ordinal of U
proof
percases ( x in dom f or f . x = 0 ) by FUNCT_1:def_2;
suppose x in dom f ; ::_thesis: f . x is Ordinal of U
then  x in a by FUNCT_2:def_1;
then  f . x in On U by FUNCT_2:5;
hence  f . x is Ordinal of U by ORDINAL1:def_9; ::_thesis: verum
end;
suppose f . x = 0 ; ::_thesis: f . x is Ordinal of U
hence  f . x is Ordinal of U by CLASSES2:56; ::_thesis: verum
end;
end;
end;
end;

theorem Th41: :: ORDINAL6:41
for a being ordinal number
for U being Universe st a in U holds
for f being Ordinal-Sequence of a,U holds Union f in U
proof
let a be ordinal number ; ::_thesis: for U being Universe st a in U holds
for f being Ordinal-Sequence of a,U holds Union f in U
let U be Universe; ::_thesis: ( a in U implies for f being Ordinal-Sequence of a,U holds Union f in U )
assume A1: a in U ; ::_thesis: for f being Ordinal-Sequence of a,U holds Union f in U
let f be Ordinal-Sequence of a,U; ::_thesis: Union f in U
 dom f = a by FUNCT_2:def_1;
then  ( card (dom f) in card U & card (rng f) c= card (dom f) & rng f c= On U & On U c= U ) by A1, CARD_2:61, CLASSES2:1, ORDINAL2:7, RELAT_1:def_19;
then  ( card (rng f) in card U & rng f c= U ) by ORDINAL1:12, XBOOLE_1:1;
then  rng f in U by CLASSES1:1;
hence  Union f in U by CLASSES2:59; ::_thesis: verum
end;

theorem Th42: :: ORDINAL6:42
for a being ordinal number
for U being Universe st a in U holds
for f being Ordinal-Sequence of a,U holds sup f in U
proof
let a be ordinal number ; ::_thesis: for U being Universe st a in U holds
for f being Ordinal-Sequence of a,U holds sup f in U
let U be Universe; ::_thesis: ( a in U implies for f being Ordinal-Sequence of a,U holds sup f in U )
assume A1: a in U ; ::_thesis: for f being Ordinal-Sequence of a,U holds sup f in U
let f be Ordinal-Sequence of a,U; ::_thesis: sup f in U
reconsider u = Union f as Ordinal of U by Th41, A1;
 On (rng f) = rng f by Th2;
then  sup f c= succ u by ORDINAL3:72;
hence  sup f in U by CLASSES1:def_1; ::_thesis: verum
end;

scheme :: ORDINAL6:sch 1
CriticalNumber2{ F1() ->  Universe, F2() ->  Ordinal of F1(), F3() ->  Ordinal-Sequence of omega,F1(), F4( Ordinal) ->  Ordinal } :
 ( F2() c= Union F3() & F4((Union F3())) = Union F3() & ( for b being ordinal number st F2() c= b & b in F1() & F4(b) = b holds
Union F3() c= b ) )
provided
A1: omega in F1() and
A2: for a being ordinal number st a in F1() holds
F4(a) in F1() and
A3: for a, b being ordinal number st a in b & b in F1() holds
F4(a) in F4(b) and
A4: for a being Ordinal of F1() st not a is empty & a is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = a & ( for b being ordinal number st b in a holds
phi . b = F4(b) ) holds
F4(a) is_limes_of phi and
A5: F3() . 0 = F2() and
A6: for a being ordinal number st a in omega holds
F3() . (succ a) = F4((F3() . a))
proof
A7: dom F3() = omega by FUNCT_2:def_1;
A8: F2() in rng F3() by A5, A7, FUNCT_1:def_3;
hence  F2() c= Union F3() by ZFMISC_1:74; ::_thesis: ( F4((Union F3())) = Union F3() & ( for b being ordinal number st F2() c= b & b in F1() & F4(b) = b holds
Union F3() c= b ) )
set phi = F3();
A9: now__::_thesis:_for_a_being_ordinal_number_holds_not_S1[a]
defpred S1[ Ordinal] means ( $1 in F1() & $1 c/= F4($1) );
assume A10: ex a being ordinal number st S1[a] ; ::_thesis: contradiction
consider a being ordinal number  such that
A11: S1[a] and
A12: for b being ordinal number st S1[b] holds
a c= b from ORDINAL1:sch_1(A10);
 F4(F4(a)) in F4(a) by A3, A11, ORDINAL1:16;
then  F4(a) c/= F4(F4(a)) by ORDINAL1:5;
hence  contradiction by A2, A11, A12; ::_thesis: verum
end;
then  F2() c= F4(F2()) ;
then A13: ( F2() c< F4(F2()) or F2() = F4(F2()) ) by XBOOLE_0:def_8;
percases ( F4(F2()) = F2() or F2() in F4(F2()) ) by A13, ORDINAL1:11;
supposeA14: F4(F2()) = F2() ; ::_thesis: ( F4((Union F3())) = Union F3() & ( for b being ordinal number st F2() c= b & b in F1() & F4(b) = b holds
Union F3() c= b ) )
A15: for a being set st a in omega holds
F3() . a = F2()
proof
let a be set ; ::_thesis: ( a in omega implies F3() . a = F2() )
assume  a in omega ; ::_thesis: F3() . a = F2()
then reconsider a = a as Element of omega ;
defpred S1[ Nat] means F3() . $1 = F2();
A16: S1[ 0 ] by A5;
A17: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A18: S1[n] ; ::_thesis: S1[n + 1]
 n in omega by ORDINAL1:def_12;
then  F3() . (succ n) = F4(F2()) by A6, A18;
hence  S1[n + 1] by A14, NAT_1:38; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A16, A17);
then  S1[a] ;
hence  F3() . a = F2() ; ::_thesis: verum
end;
 rng F3() = {F2()}
proof
thus  rng F3() c= {F2()} :: according to XBOOLE_0:def_10 ::_thesis: {F2()} c= rng F3()
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng F3() or x in {F2()} )
assume  x in rng F3() ; ::_thesis: x in {F2()}
then consider a being set  such that
A19: ( a in dom F3() & x = F3() . a ) by FUNCT_1:def_3;
 x = F2() by A15, A19, A7;
hence  x in {F2()} by TARSKI:def_1; ::_thesis: verum
end;
thus  {F2()} c= rng F3() by A8, ZFMISC_1:31; ::_thesis: verum
end;
then  Union F3() = F2() by ZFMISC_1:25;
hence  ( F4((Union F3())) = Union F3() & ( for b being ordinal number st F2() c= b & b in F1() & F4(b) = b holds
Union F3() c= b ) ) by A14; ::_thesis: verum
end;
supposeA20: F2() in F4(F2()) ; ::_thesis: ( F4((Union F3())) = Union F3() & ( for b being ordinal number st F2() c= b & b in F1() & F4(b) = b holds
Union F3() c= b ) )
deffunc H1( Ordinal, Ordinal) ->  Ordinal = F4($2);
deffunc H2( Ordinal, T-Sequence) ->  set = {} ;
A21: now__::_thesis:_for_a_being_ordinal_number_st_succ_a_in_omega_holds_
F3()_._(succ_a)_=_H1(a,F3()_._a)
let a be ordinal number ; ::_thesis: ( succ a in omega implies F3() . (succ a) = H1(a,F3() . a) )
assume A22: succ a in omega ; ::_thesis: F3() . (succ a) = H1(a,F3() . a)
 a in succ a by ORDINAL1:6;
hence  F3() . (succ a) = H1(a,F3() . a) by A6, A22, ORDINAL1:10; ::_thesis: verum
end;
A23: for a being ordinal number st a in omega holds
( F2() c= F3() . a & F3() . a in F3() . (succ a) )
proof
let a be ordinal number ; ::_thesis: ( a in omega implies ( F2() c= F3() . a & F3() . a in F3() . (succ a) ) )
assume  a in omega ; ::_thesis: ( F2() c= F3() . a & F3() . a in F3() . (succ a) )
then reconsider a = a as Element of omega ;
defpred S1[ Nat] means ( F2() c= F3() . $1 & F3() . $1 in F3() . (succ $1) );
A24: S1[ 0 ] by A20, A5, A6;
A25: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A26: S1[n] ; ::_thesis: S1[n + 1]
A27: ( n + 1 = succ n & (n + 1) + 1 = succ (n + 1) & n + 1 in omega & (n + 1) + 1 in omega ) by NAT_1:38;
then  ( F3() . (n + 1) = F4((F3() . n)) & F3() . ((n + 1) + 1) = F4((F3() . (n + 1))) ) by A21;
then  ( F3() . n c= F3() . (n + 1) & F3() . (n + 1) in F3() . ((n + 1) + 1) ) by A3, A9, A26, A27;
hence  S1[n + 1] by A26, NAT_1:38, XBOOLE_1:1; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A24, A25);
then  S1[a] ;
hence  ( F2() c= F3() . a & F3() . a in F3() . (succ a) ) ; ::_thesis: verum
end;
deffunc H3( Ordinal) ->  Ordinal = F4($1);
consider fi being Ordinal-Sequence such that
A28: ( dom fi = Union F3() & ( for a being ordinal number st a in Union F3() holds
fi . a = H3(a) ) ) from ORDINAL2:sch_3();
 1 = succ 0 ;
then  F3() . 1 = H3(F2()) by A5, A6;
then  H3(F2()) in rng F3() by A7, FUNCT_1:def_3;
then A29: H3(F2()) c= Union F3() by ZFMISC_1:74;
A30: Union F3() in F1() by A1, Th41;
now__::_thesis:_for_c_being_ordinal_number_st_c_in_Union_F3()_holds_
succ_c_in_Union_F3()
let c be ordinal number ; ::_thesis: ( c in Union F3() implies succ c in Union F3() )
assume  c in Union F3() ; ::_thesis: succ c in Union F3()
then consider x being set  such that
A31: ( x in dom F3() & c in F3() . x ) by CARD_5:2;
reconsider x = x as Element of omega by A31, FUNCT_2:def_1;
 ( succ c c= F3() . x & F3() . x in F3() . (succ x) ) by A23, A31, ORDINAL1:21;
then  ( succ c in F3() . (succ x) & succ x in omega ) by ORDINAL1:12;
hence  succ c in Union F3() by A7, CARD_5:2; ::_thesis: verum
end;
then A32: Union F3() is limit_ordinal by ORDINAL1:28;
then A33: H3( Union F3()) is_limes_of fi by A4, A20, A28, A29, A30;
 fi is increasing
proof
let a be ordinal number ; :: according to ORDINAL2:def_12 ::_thesis: for b1 being set holds
( not a in b1 or not b1 in dom fi or fi . a in fi . b1 )
let b be ordinal number ; ::_thesis: ( not a in b or not b in dom fi or fi . a in fi . b )
assume A34: ( a in b & b in dom fi ) ; ::_thesis: fi . a in fi . b
then  ( fi . a = H3(a) & fi . b = H3(b) & b in F1() ) by A30, A28, ORDINAL1:10;
hence  fi . a in fi . b by A3, A34; ::_thesis: verum
end;
then A35: sup fi = lim fi by A20, A28, A29, A32, ORDINAL4:8
.= H3( Union F3()) by A33, ORDINAL2:def_10 ;
thus  H3( Union F3()) c= Union F3() :: according to XBOOLE_0:def_10 ::_thesis: ( Union F3() c= F4((Union F3())) & ( for b being ordinal number st F2() c= b & b in F1() & F4(b) = b holds
Union F3() c= b ) )
proof
let x be Ordinal; :: according to ORDINAL1:def_5 ::_thesis: ( not x in H3( Union F3()) or x in Union F3() )
assume A36: x in H3( Union F3()) ; ::_thesis: x in Union F3()
reconsider A = x as Ordinal ;
consider b being ordinal number  such that
A37: ( b in rng fi & A c= b ) by A35, A36, ORDINAL2:21;
consider y being set  such that
A38: ( y in dom fi & b = fi . y ) by A37, FUNCT_1:def_3;
reconsider y = y as Ordinal by A38;
consider z being set  such that
A39: ( z in dom F3() & y in F3() . z ) by A28, A38, CARD_5:2;
reconsider z = z as Ordinal by A39;
set c = F3() . z;
 succ z in omega by A7, A39, ORDINAL1:28;
then A40: ( F3() . (succ z) = H3(F3() . z) & F3() . (succ z) in rng F3() & b = H3(y) ) by A7, A21, A28, A38, FUNCT_1:def_3;
 ( b in H3(F3() . z) & H3(F3() . z) c= Union F3() ) by A40, A3, A39, ZFMISC_1:74;
hence  x in Union F3() by A37, ORDINAL1:12; ::_thesis: verum
end;
thus  Union F3() c= H3( Union F3()) by A9, A1, Th41; ::_thesis: for b being ordinal number st F2() c= b & b in F1() & F4(b) = b holds
Union F3() c= b
let b be ordinal number ; ::_thesis: ( F2() c= b & b in F1() & F4(b) = b implies Union F3() c= b )
assume A41: ( F2() c= b & b in F1() & H3(b) = b ) ; ::_thesis: Union F3() c= b
 rng F3() c= b
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng F3() or x in b )
assume  x in rng F3() ; ::_thesis: x in b
then consider a being set  such that
A42: ( a in dom F3() & x = F3() . a ) by FUNCT_1:def_3;
reconsider a = a as Element of omega by A42, FUNCT_2:def_1;
defpred S1[ Nat] means F3() . $1 in b;
 F2() <> b by A20, A41;
then  F2() c< b by A41, XBOOLE_0:def_8;
then A43: S1[ 0 ] by A5, ORDINAL1:11;
A44: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  S1[n] ; ::_thesis: S1[n + 1]
then  ( H3(F3() . n) in b & n in omega ) by A3, A41, ORDINAL1:def_12;
then  F3() . (succ n) in b by A6;
hence  S1[n + 1] by NAT_1:38; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A43, A44);
then  S1[a] ;
hence  x in b by A42; ::_thesis: verum
end;
then  ( Union F3() c= union b & union b c= b ) by ORDINAL2:5, ZFMISC_1:77;
hence  Union F3() c= b by XBOOLE_1:1; ::_thesis: verum
end;
end;
end;

Lm1:  {} in omega
by ORDINAL1:def_11;

scheme :: ORDINAL6:sch 2
CriticalNumber3{ F1() ->  Universe, F2() ->  Ordinal of F1(), F3( Ordinal) ->  Ordinal } :
 ex a being Ordinal of F1() st
( F2() in a & F3(a) = a )
provided
A1: omega in F1() and
A2: for a being ordinal number st a in F1() holds
F3(a) in F1() and
A3: for a, b being ordinal number st a in b & b in F1() holds
F3(a) in F3(b) and
A4: for a being Ordinal of F1() st not a is empty & a is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = a & ( for b being ordinal number st b in a holds
phi . b = F3(b) ) holds
F3(a) is_limes_of phi
proof
assume A5: for a being Ordinal of F1() holds
( not F2() in a or not F3(a) = a ) ; ::_thesis: contradiction
deffunc H1( Ordinal, Ordinal) ->  Ordinal = F3($2);
deffunc H2( Ordinal, T-Sequence) ->  set = {} ;
consider phi being Ordinal-Sequence such that
A6: dom phi = omega and
A7: ( {} in omega implies phi . {} = succ F2() ) and
A8: for a being ordinal number st succ a in omega holds
phi . (succ a) = H1(a,phi . a) and
 for a being ordinal number st a in omega & a <> {} & a is limit_ordinal holds
phi . a = H2(a,phi | a) from ORDINAL2:sch_11();
A9: rng phi c= On F1()
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng phi or y in On F1() )
assume  y in rng phi ; ::_thesis: y in On F1()
then consider x being set  such that
A10: ( x in dom phi & y = phi . x ) by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A6, A10;
defpred S1[ Nat] means phi . $1 in On F1();
A11: S1[ 0 ] by A7, ORDINAL1:def_9;
A12: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  S1[n] ; ::_thesis: S1[n + 1]
then A13: phi . n in F1() by ORDINAL1:def_9;
A14: n + 1 = succ n by NAT_1:38;
 ( phi . (n + 1) = F3((phi . n)) & F3((phi . n)) in F1() ) by A8, A14, A13, A2;
hence  S1[n + 1] by ORDINAL1:def_9; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A11, A12);
then  S1[x] ;
hence  y in On F1() by A10; ::_thesis: verum
end;
then reconsider phi = phi as Ordinal-Sequence of omega,F1() by A6, FUNCT_2:2;
A15: now__::_thesis:_for_a_being_ordinal_number_holds_not_S1[a]
defpred S1[ Ordinal] means ( $1 in F1() & $1 c/= F3($1) );
assume A16: ex a being ordinal number st S1[a] ; ::_thesis: contradiction
consider a being ordinal number  such that
A17: S1[a] and
A18: for b being ordinal number st S1[b] holds
a c= b from ORDINAL1:sch_1(A16);
 F3(F3(a)) in F3(a) by A3, A17, ORDINAL1:16;
then  F3(a) c/= F3(F3(a)) by ORDINAL1:5;
hence  contradiction by A17, A18, A2; ::_thesis: verum
end;
A19: now__::_thesis:_for_a_being_ordinal_number_st_F2()_in_a_&_a_in_F1()_holds_
a_in_F3(a)
let a be ordinal number ; ::_thesis: ( F2() in a & a in F1() implies a in F3(a) )
assume  ( F2() in a & a in F1() ) ; ::_thesis: a in F3(a)
then  ( a c= F3(a) & a <> F3(a) ) by A5, A15;
then  a c< F3(a) by XBOOLE_0:def_8;
hence  a in F3(a) by ORDINAL1:11; ::_thesis: verum
end;
A20: for a being ordinal number st a in omega holds
F2() in phi . a
proof
let a be ordinal number ; ::_thesis: ( a in omega implies F2() in phi . a )
assume  a in omega ; ::_thesis: F2() in phi . a
then reconsider a = a as Element of omega ;
defpred S1[ Nat] means F2() in phi . $1;
A21: S1[ 0 ] by A7, ORDINAL1:6;
A22: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A23: S1[n] ; ::_thesis: S1[n + 1]
 ( n + 1 = succ n & n + 1 in omega ) by NAT_1:38;
then  phi . (n + 1) = F3((phi . n)) by A8;
then  phi . n in phi . (n + 1) by A23, A19;
hence  S1[n + 1] by A23, ORDINAL1:10; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A21, A22);
then  S1[a] ;
hence  F2() in phi . a ; ::_thesis: verum
end;
A24: phi is increasing
proof
let a be ordinal number ; :: according to ORDINAL2:def_12 ::_thesis: for b1 being set holds
( not a in b1 or not b1 in dom phi or phi . a in phi . b1 )
let b be ordinal number ; ::_thesis: ( not a in b or not b in dom phi or phi . a in phi . b )
assume A25: ( a in b & b in dom phi ) ; ::_thesis: phi . a in phi . b
then A26: ex c being ordinal number st
( b = a +^ c & c <> {} ) by ORDINAL3:28;
defpred S1[ Ordinal] means ( a +^ $1 in omega & $1 <> {} implies phi . a in phi . (a +^ $1) );
A27: S1[ {} ] ;
A28: for c being ordinal number st S1[c] holds
S1[ succ c]
proof
let c be ordinal number ; ::_thesis: ( S1[c] implies S1[ succ c] )
assume that
A29: ( a +^ c in omega & c <> {} implies phi . a in phi . (a +^ c) ) and
A30: ( a +^ (succ c) in omega & succ c <> {} ) ; ::_thesis: phi . a in phi . (a +^ (succ c))
A31: ( a +^ c in succ (a +^ c) & a +^ (succ c) = succ (a +^ c) ) by ORDINAL1:6, ORDINAL2:28;
reconsider d = phi . (a +^ c) as Ordinal ;
 a +^ c in omega by A30, A31, ORDINAL1:10;
then  ( phi . (a +^ (succ c)) = F3(d) & d in F3(d) & a +^ {} = a ) by A8, A19, A30, A31, A20, ORDINAL2:27;
hence  phi . a in phi . (a +^ (succ c)) by A29, A30, A31, ORDINAL1:10; ::_thesis: verum
end;
A32: for b being ordinal number st b <> {} & b is limit_ordinal & ( for c being ordinal number st c in b holds
S1[c] ) holds
S1[b]
proof
let b be ordinal number ; ::_thesis: ( b <> {} & b is limit_ordinal & ( for c being ordinal number st c in b holds
S1[c] ) implies S1[b] )
assume that
A33: ( b <> {} & b is limit_ordinal ) and
 for c being ordinal number st c in b & a +^ c in omega & c <> {} holds
phi . a in phi . (a +^ c) and
A34: ( a +^ b in omega & b <> {} ) ; ::_thesis: phi . a in phi . (a +^ b)
 a +^ b <> {} by A34, ORDINAL3:26;
then  ( a +^ b is limit_ordinal & {} in a +^ b ) by A33, ORDINAL3:8, ORDINAL3:29;
hence  phi . a in phi . (a +^ b) by A34; ::_thesis: verum
end;
 for c being ordinal number holds S1[c] from ORDINAL2:sch_1(A27, A28, A32);
hence  phi . a in phi . b by A6, A25, A26; ::_thesis: verum
end;
A35: sup phi in F1() by A1, Th42;
deffunc H3( Ordinal) ->  Ordinal = F3($1);
consider fi being Ordinal-Sequence such that
A36: ( dom fi = sup phi & ( for a being ordinal number st a in sup phi holds
fi . a = H3(a) ) ) from ORDINAL2:sch_3();
 ( succ F2() in rng phi & sup (rng phi) = sup phi ) by A6, A7, Lm1, FUNCT_1:def_3;
then A37: ( sup phi <> {} & sup phi is limit_ordinal ) by A6, A24, ORDINAL2:19, ORDINAL4:16;
then A38: H3( sup phi) is_limes_of fi by A35, A4, A36;
 fi is increasing
proof
let a be ordinal number ; :: according to ORDINAL2:def_12 ::_thesis: for b1 being set holds
( not a in b1 or not b1 in dom fi or fi . a in fi . b1 )
let b be ordinal number ; ::_thesis: ( not a in b or not b in dom fi or fi . a in fi . b )
assume A39: ( a in b & b in dom fi ) ; ::_thesis: fi . a in fi . b
then  ( fi . a = H3(a) & fi . b = H3(b) & b in F1() ) by A35, A36, ORDINAL1:10;
hence  fi . a in fi . b by A3, A39; ::_thesis: verum
end;
then A40: sup fi = lim fi by A36, A37, ORDINAL4:8
.= H3( sup phi) by A38, ORDINAL2:def_10 ;
A41: sup fi c= sup phi
proof
let x be Ordinal; :: according to ORDINAL1:def_5 ::_thesis: ( not x in sup fi or x in sup phi )
assume A42: x in sup fi ; ::_thesis: x in sup phi
reconsider A = x as Ordinal ;
consider b being ordinal number  such that
A43: ( b in rng fi & A c= b ) by A42, ORDINAL2:21;
consider y being set  such that
A44: ( y in dom fi & b = fi . y ) by A43, FUNCT_1:def_3;
reconsider y = y as Ordinal by A44;
consider c being ordinal number  such that
A45: ( c in rng phi & y c= c ) by A36, A44, ORDINAL2:21;
A46: c in F1() by A9, A45, ORDINAL1:def_9;
consider z being set  such that
A47: ( z in dom phi & c = phi . z ) by A45, FUNCT_1:def_3;
reconsider z = z as Ordinal by A47;
 succ z in omega by A6, A47, ORDINAL1:28;
then A48: ( phi . (succ z) = H3(c) & phi . (succ z) in rng phi & b = H3(y) ) by A6, A8, A36, A44, A47, FUNCT_1:def_3;
 ( y c< c iff ( y <> c & y c= c ) ) by XBOOLE_0:def_8;
then  ( H3(y) in H3(c) or y = c ) by A46, A3, A45, ORDINAL1:11;
then  ( b c= H3(c) & H3(c) in sup phi ) by A48, ORDINAL1:def_2, ORDINAL2:19;
then  b in sup phi by ORDINAL1:12;
hence  x in sup phi by A43, ORDINAL1:12; ::_thesis: verum
end;
 phi . 0 in rng phi by A6, FUNCT_1:def_3;
then  ( F2() in phi . 0 & phi . 0 in sup phi ) by A20, ORDINAL2:19;
then  F2() in sup phi by ORDINAL1:10;
hence  contradiction by A35, A19, A40, A41, ORDINAL1:5; ::_thesis: verum
end;


theorem Th43: :: ORDINAL6:43
for b being ordinal number
for W being Universe
for phi being normal Ordinal-Sequence of W st omega in W & b in W holds
ex a being ordinal number st
( b in a & a is_a_fixpoint_of phi )
proof
let b be ordinal number ; ::_thesis: for W being Universe
for phi being normal Ordinal-Sequence of W st omega in W & b in W holds
ex a being ordinal number st
( b in a & a is_a_fixpoint_of phi )
let W be Universe; ::_thesis: for phi being normal Ordinal-Sequence of W st omega in W & b in W holds
ex a being ordinal number st
( b in a & a is_a_fixpoint_of phi )
let phi be normal Ordinal-Sequence of W; ::_thesis: ( omega in W & b in W implies ex a being ordinal number st
( b in a & a is_a_fixpoint_of phi ) )
assume that
A1: omega in W and
A2: b in W ; ::_thesis: ex a being ordinal number st
( b in a & a is_a_fixpoint_of phi )
reconsider b1 = b as Ordinal of W by A2;
A3: dom phi = On W by FUNCT_2:def_1;
deffunc H1( set ) ->  Ordinal of W = phi . $1;
A4: for a being ordinal number st a in W holds
H1(a) in W ;
A5: for a, b being ordinal number st a in b & b in W holds
H1(a) in H1(b)
proof
let a, b be ordinal number ; ::_thesis: ( a in b & b in W implies H1(a) in H1(b) )
 ( b in W implies b in dom phi ) by A3, ORDINAL1:def_9;
hence  ( a in b & b in W implies H1(a) in H1(b) ) by ORDINAL2:def_12; ::_thesis: verum
end;
A6: for a being Ordinal of W st not a is empty & a is limit_ordinal holds
for f being Ordinal-Sequence st dom f = a & ( for b being ordinal number st b in a holds
f . b = H1(b) ) holds
H1(a) is_limes_of f
proof
let a be Ordinal of W; ::_thesis: ( not a is empty & a is limit_ordinal implies for f being Ordinal-Sequence st dom f = a & ( for b being ordinal number st b in a holds
f . b = H1(b) ) holds
H1(a) is_limes_of f )
assume A7: ( not a is empty & a is limit_ordinal ) ; ::_thesis: for f being Ordinal-Sequence st dom f = a & ( for b being ordinal number st b in a holds
f . b = H1(b) ) holds
H1(a) is_limes_of f
let f be Ordinal-Sequence; ::_thesis: ( dom f = a & ( for b being ordinal number st b in a holds
f . b = H1(b) ) implies H1(a) is_limes_of f )
assume that
A8: dom f = a and
A9: for b being ordinal number st b in a holds
f . b = H1(b) ; ::_thesis: H1(a) is_limes_of f
A10: a in dom phi by A3, ORDINAL1:def_9;
then  a c= dom phi by ORDINAL1:def_2;
then A11: dom (phi | a) = a by RELAT_1:62;
now__::_thesis:_for_x_being_set_st_x_in_a_holds_
(phi_|_a)_._x_=_f_._x
let x be set ; ::_thesis: ( x in a implies (phi | a) . x = f . x )
assume A12: x in a ; ::_thesis: (phi | a) . x = f . x
hence (phi | a) . x = H1(x) by FUNCT_1:49
.= f . x by A12, A9 ;
::_thesis: verum
end;
then  f = phi | a by A8, A11, FUNCT_1:2;
hence  H1(a) is_limes_of f by A7, A10, ORDINAL2:def_13; ::_thesis: verum
end;
consider a being Ordinal of W such that
A13: ( b1 in a & H1(a) = a ) from ORDINAL6:sch_2(A1, A4, A5, A6);
take  a ; ::_thesis: ( b in a & a is_a_fixpoint_of phi )
thus  ( b in a & a in dom phi & a = phi . a ) by A3, A13, ORDINAL1:def_9; :: according to ABIAN:def_3 ::_thesis: verum
end;

theorem Th44: :: ORDINAL6:44
for W being Universe
for F being normal Ordinal-Sequence of W st omega in W holds
criticals F is Ordinal-Sequence of W
proof
let W be Universe; ::_thesis: for F being normal Ordinal-Sequence of W st omega in W holds
criticals F is Ordinal-Sequence of W
let F be normal Ordinal-Sequence of W; ::_thesis: ( omega in W implies criticals F is Ordinal-Sequence of W )
assume A1: omega in W ; ::_thesis: criticals F is Ordinal-Sequence of W
set G = criticals F;
A2: ( dom F = On W & rng F c= On W ) by FUNCT_2:def_1, RELAT_1:def_19;
A3: rng (criticals F) c= rng F by Th30;
then A4: rng (criticals F) c= On W by A2, XBOOLE_1:1;
 dom (criticals F) = On W
proof
thus  dom (criticals F) c= On W by A2, Th32; :: according to XBOOLE_0:def_10 ::_thesis: On W c= dom (criticals F)
let a be ordinal number ; :: according to ORDINAL1:def_5 ::_thesis: ( not a in On W or a in dom (criticals F) )
assume  a in On W ; ::_thesis: a in dom (criticals F)
then A5: a in W by ORDINAL1:def_9;
defpred S1[ Ordinal] means ( $1 in W implies $1 in dom (criticals F) );
consider a0 being Ordinal such that
A6: ( 0-element_of W in a0 & a0 is_a_fixpoint_of F ) by A1, Th43;
consider a1 being Ordinal such that
A7: ( a1 in dom (criticals F) & a0 = (criticals F) . a1 ) by A6, Th33;
A8: S1[ {} ] by A7, ORDINAL1:12, XBOOLE_1:2;
A9: for a being ordinal number st S1[a] holds
S1[ succ a]
proof
let a be ordinal number ; ::_thesis: ( S1[a] implies S1[ succ a] )
assume A10: ( S1[a] & succ a in W ) ; ::_thesis: succ a in dom (criticals F)
A11: a c= succ a by ORDINAL3:1;
then  (criticals F) . a in rng (criticals F) by A10, CLASSES1:def_1, FUNCT_1:def_3;
then  (criticals F) . a in W by A4, ORDINAL1:def_9;
then consider b being ordinal number  such that
A12: ( (criticals F) . a in b & b is_a_fixpoint_of F ) by A1, Th43;
consider c being ordinal number  such that
A13: ( c in dom (criticals F) & b = (criticals F) . c ) by A12, Th33;
 a in c by A10, A11, A12, A13, Th23, CLASSES1:def_1;
then  succ a c= c by ORDINAL1:21;
hence  succ a in dom (criticals F) by A13, ORDINAL1:12; ::_thesis: verum
end;
A14: for a being ordinal number st a <> {} & a is limit_ordinal & ( for b being ordinal number st b in a holds
S1[b] ) holds
S1[a]
proof
let a be ordinal number ; ::_thesis: ( a <> {} & a is limit_ordinal & ( for b being ordinal number st b in a holds
S1[b] ) implies S1[a] )
assume that
A15: ( a <> {} & a is limit_ordinal ) and
A16: for b being ordinal number st b in a holds
S1[b] and
A17: a in W ; ::_thesis: a in dom (criticals F)
set X = (criticals F) .: a;
 ( card ((criticals F) .: a) c= card a & card a c= a ) by CARD_1:8, CARD_1:67;
then  card ((criticals F) .: a) c= a by XBOOLE_1:1;
then  card ((criticals F) .: a) in W by A17, CLASSES1:def_1;
then  card ((criticals F) .: a) in On W by ORDINAL1:def_9;
then A18: card ((criticals F) .: a) in card W by CLASSES2:9;
A19: (criticals F) .: a c= rng (criticals F) by RELAT_1:111;
then A20: (criticals F) .: a c= On W by A4, XBOOLE_1:1;
reconsider u = union ((criticals F) .: a) as Ordinal by A19, A4, ORDINAL3:4, XBOOLE_1:1;
 On W c= W by ORDINAL2:7;
then  (criticals F) .: a c= W by A20, XBOOLE_1:1;
then  (criticals F) .: a in W by A18, CLASSES1:1;
then  u in W by CLASSES2:59;
then consider b being ordinal number  such that
A21: ( u in b & b is_a_fixpoint_of F ) by A1, Th43;
A22: a c= dom (criticals F)
proof
let c be ordinal number ; :: according to ORDINAL1:def_5 ::_thesis: ( not c in a or c in dom (criticals F) )
assume A23: c in a ; ::_thesis: c in dom (criticals F)
then  c in W by A17, ORDINAL1:10;
hence  c in dom (criticals F) by A16, A23; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_a_holds_
(criticals_F)_._x_in_b
let x be set ; ::_thesis: ( x in a implies (criticals F) . x in b )
assume A24: x in a ; ::_thesis: (criticals F) . x in b
then  (criticals F) . x in (criticals F) .: a by A22, FUNCT_1:def_6;
then  ( (criticals F) . x is Ordinal & (criticals F) . x c= u ) by A24, ZFMISC_1:74;
hence  (criticals F) . x in b by A21, ORDINAL1:12; ::_thesis: verum
end;
hence  a in dom (criticals F) by A15, A22, A21, Th38; ::_thesis: verum
end;
 for b being ordinal number holds S1[b] from ORDINAL2:sch_1(A8, A9, A14);
hence  a in dom (criticals F) by A5; ::_thesis: verum
end;
hence  criticals F is Ordinal-Sequence of W by A3, A2, FUNCT_2:2, XBOOLE_1:1; ::_thesis: verum
end;

theorem Th45: :: ORDINAL6:45
for f being Ordinal-Sequence st f is normal holds
for a being ordinal number st a in dom (criticals f) holds
f . a c= (criticals f) . a
proof
let f be Ordinal-Sequence; ::_thesis: ( f is normal implies for a being ordinal number st a in dom (criticals f) holds
f . a c= (criticals f) . a )
assume A1: f is normal ; ::_thesis: for a being ordinal number st a in dom (criticals f) holds
f . a c= (criticals f) . a
set g = criticals f;
A2: dom (criticals f) c= dom f by Th32;
defpred S1[ Ordinal] means ( $1 in dom (criticals f) implies f . $1 c= (criticals f) . $1 );
A3: S1[ {} ]
proof
assume  {} in dom (criticals f) ; ::_thesis: f . {} c= (criticals f) . {}
then  (criticals f) . 0 is_a_fixpoint_of f by Th29;
then  ( f . ((criticals f) . 0) = (criticals f) . 0 & (criticals f) . 0 in dom f ) by ABIAN:def_3;
hence  f . {} c= (criticals f) . {} by A1, ORDINAL4:9, XBOOLE_1:2; ::_thesis: verum
end;
A4: for a being ordinal number st S1[a] holds
S1[ succ a]
proof
let a be ordinal number ; ::_thesis: ( S1[a] implies S1[ succ a] )
assume that
 S1[a] and
A5: succ a in dom (criticals f) ; ::_thesis: f . (succ a) c= (criticals f) . (succ a)
 (criticals f) . (succ a) is_a_fixpoint_of f by A5, Th29;
then  ( (criticals f) . (succ a) in dom f & f . ((criticals f) . (succ a)) = (criticals f) . (succ a) ) by ABIAN:def_3;
hence  f . (succ a) c= (criticals f) . (succ a) by A1, A5, ORDINAL4:9, ORDINAL4:10; ::_thesis: verum
end;
A6: for a being ordinal number st a <> {} & a is limit_ordinal & ( for b being ordinal number st b in a holds
S1[b] ) holds
S1[a]
proof
let a be ordinal number ; ::_thesis: ( a <> {} & a is limit_ordinal & ( for b being ordinal number st b in a holds
S1[b] ) implies S1[a] )
assume that
A7: ( a <> {} & a is limit_ordinal ) and
A8: for b being ordinal number st b in a holds
S1[b] and
A9: a in dom (criticals f) ; ::_thesis: f . a c= (criticals f) . a
 ( f . a is_limes_of f | a & (criticals f) . a is_limes_of (criticals f) | a ) by A1, A2, A7, A9, ORDINAL2:def_13;
then A10: ( f . a = lim (f | a) & (criticals f) . a = lim ((criticals f) | a) ) by ORDINAL2:def_10;
A11: ( f | a is increasing & (criticals f) | a is increasing ) by A1, ORDINAL4:15;
A12: ( a c= dom f & a c= dom (criticals f) ) by A2, A9, ORDINAL1:def_2;
then A13: ( dom (f | a) = a & dom ((criticals f) | a) = a ) by RELAT_1:62;
then  ( Union (f | a) is_limes_of f | a & Union ((criticals f) | a) is_limes_of (criticals f) | a ) by A7, A11, ORDINAL5:6;
then A14: ( f . a = Union (f | a) & (criticals f) . a = Union ((criticals f) | a) ) by A10, ORDINAL2:def_10;
let b be ordinal number ; :: according to ORDINAL1:def_5 ::_thesis: ( not b in f . a or b in (criticals f) . a )
assume  b in f . a ; ::_thesis: b in (criticals f) . a
then consider x being set  such that
A15: ( x in a & b in (f | a) . x ) by A13, A14, CARD_5:2;
 ( (f | a) . x = f . x & ((criticals f) | a) . x = (criticals f) . x & f . x c= (criticals f) . x ) by A12, A8, A15, FUNCT_1:49;
hence  b in (criticals f) . a by A15, A13, A14, CARD_5:2; ::_thesis: verum
end;
thus  for a being ordinal number holds S1[a] from ORDINAL2:sch_1(A3, A4, A6); ::_thesis: verum
end;

begin

definition
let U be Universe;
let a, b be Ordinal of U;
:: original: exp
redefine func exp (a,b) ->  Ordinal of U;
coherence
 exp (a,b) is Ordinal of U
proof
percases ( ( a = 0 & b = 0 ) or ( a = 0 & b <> 0 ) or 0 in a ) by ORDINAL3:8;
suppose ( a = 0 & b = 0 ) ; ::_thesis: exp (a,b) is Ordinal of U
then  exp (a,b) = 1-element_of U by ORDINAL2:43;
hence  exp (a,b) is Ordinal of U ; ::_thesis: verum
end;
suppose ( a = 0 & b <> 0 ) ; ::_thesis: exp (a,b) is Ordinal of U
hence  exp (a,b) is Ordinal of U by ORDINAL4:20; ::_thesis: verum
end;
supposeA1: 0 in a ; ::_thesis: exp (a,b) is Ordinal of U
defpred S1[ Ordinal] means ( $1 in U implies exp (a,$1) in U );
 exp (a,0) = succ 0 by ORDINAL2:43;
then A2: S1[ {} ] by CLASSES2:5;
A3: for b being ordinal number st S1[b] holds
S1[ succ b]
proof
let b be ordinal number ; ::_thesis: ( S1[b] implies S1[ succ b] )
assume that
A4: S1[b] and
A5: succ b in U ; ::_thesis: exp (a,(succ b)) in U
 b in succ b by ORDINAL1:6;
then reconsider b = b as Ordinal of U by A5, ORDINAL1:10;
reconsider ab = exp (a,b) as Ordinal of U by A4;
 exp (a,(succ b)) = a *^ ab by ORDINAL2:44;
hence  exp (a,(succ b)) in U ; ::_thesis: verum
end;
A6: for b being ordinal number st b <> {} & b is limit_ordinal & ( for c being ordinal number st c in b holds
S1[c] ) holds
S1[b]
proof
let b be ordinal number ; ::_thesis: ( b <> {} & b is limit_ordinal & ( for c being ordinal number st c in b holds
S1[c] ) implies S1[b] )
assume that
A7: ( b <> {} & b is limit_ordinal ) and
A8: for c being ordinal number st c in b holds
S1[c] and
A9: b in U ; ::_thesis: exp (a,b) in U
deffunc H1( Ordinal) ->  set = exp (a,$1);
consider f being Ordinal-Sequence such that
A10: ( dom f = b & ( for c being ordinal number st c in b holds
f . c = H1(c) ) ) from ORDINAL2:sch_3();
 rng f c= On U
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in On U )
assume  x in rng f ; ::_thesis: x in On U
then consider y being set  such that
A11: ( y in b & x = f . y ) by A10, FUNCT_1:def_3;
reconsider y = y as Ordinal by A11;
 ( S1[y] & y in U & x = H1(y) ) by A9, A8, A10, A11, ORDINAL1:10;
hence  x in On U by ORDINAL1:def_9; ::_thesis: verum
end;
then reconsider f = f as Ordinal-Sequence of b,U by A10, FUNCT_2:2;
A12: exp (a,b) = lim f by A7, A10, ORDINAL2:45;
 f is non-decreasing by A1, A10, ORDINAL5:8;
then  Union f is_limes_of f by A7, A10, ORDINAL5:6;
then  exp (a,b) = Union f by A12, ORDINAL2:def_10;
hence  exp (a,b) in U by A9, Th41; ::_thesis: verum
end;
 for b being ordinal number holds S1[b] from ORDINAL2:sch_1(A2, A3, A6);
hence  exp (a,b) is Ordinal of U ; ::_thesis: verum
end;
end;
end;
end;

definition
let U be Universe;
let a be ordinal number ;
assume AA: a in U ;
funcU exp a ->  Ordinal-Sequence of U means :Def8: :: ORDINAL6:def 8
 for b being Ordinal of U holds it . b = exp (a,b);
existence
 ex b1 being Ordinal-Sequence of U st
for b being Ordinal of U holds b1 . b = exp (a,b)
proof
reconsider a = a as Ordinal of U by AA;
deffunc H1( Ordinal of U) ->  Ordinal of U = exp (a,$1);
 ex f being Ordinal-Sequence of U st
for b being Ordinal of U holds f . b = H1(b) from ORDINAL4:sch_2();
hence  ex b1 being Ordinal-Sequence of U st
for b being Ordinal of U holds b1 . b = exp (a,b) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Ordinal-Sequence of U st ( for b being Ordinal of U holds b1 . b = exp (a,b) ) & ( for b being Ordinal of U holds b2 . b = exp (a,b) ) holds
b1 = b2
proof
let f1, f2 be Ordinal-Sequence of U; ::_thesis: ( ( for b being Ordinal of U holds f1 . b = exp (a,b) ) & ( for b being Ordinal of U holds f2 . b = exp (a,b) ) implies f1 = f2 )
assume that
A1: for b being Ordinal of U holds f1 . b = exp (a,b) and
A2: for b being Ordinal of U holds f2 . b = exp (a,b) ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_Element_of_On_U_holds_f1_._x_=_f2_._x
let x be Element of On U; ::_thesis: f1 . x = f2 . x
 x in U by ORDINAL1:def_9;
then  ( f1 . x = exp (a,x) & f2 . x = exp (a,x) ) by A1, A2;
hence  f1 . x = f2 . x ; ::_thesis: verum
end;
hence  f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines exp ORDINAL6:def_8_:_
 for U being Universe
for a being ordinal number st a in U holds
for b3 being Ordinal-Sequence of U holds
( b3 = U exp a iff for b being Ordinal of U holds b3 . b = exp (a,b) );

registration
cluster omega  ->  non trivial ;
coherence
 not omega is trivial ;
end;

registration
let U be Universe;
cluster epsilon-transitive epsilon-connected ordinal non trivial finite ordinal-membered for Element of U;
existence
 ex b1 being Ordinal of U st
( not b1 is trivial & b1 is finite )
proof
 not succ (1-element_of U) is trivial by NAT_2:def_1;
hence  ex b1 being Ordinal of U st
( not b1 is trivial & b1 is finite ) ; ::_thesis: verum
end;
end;

registration
cluster epsilon-transitive epsilon-connected ordinal non trivial finite ordinal-membered for set ;
existence
 ex b1 being Ordinal st
( not b1 is trivial & b1 is finite )
proof
 not 2 is trivial by NAT_2:def_1;
hence  ex b1 being Ordinal st
( not b1 is trivial & b1 is finite ) ; ::_thesis: verum
end;
end;

registration
let U be Universe;
let a be non trivial Ordinal of U;
clusterU exp a ->  normal ;
coherence
 U exp a is normal
proof
set f = U exp a;
A1: dom (U exp a) = On U by FUNCT_2:def_1;
 ( a <> 0 & a <> 1 ) by NAT_2:def_1;
then A2: 0 in a by ORDINAL3:8;
 succ 0 c= a ;
then  1 c< a by XBOOLE_0:def_8;
then A3: 1 in a by ORDINAL1:11;
A4: now__::_thesis:_for_b_being_ordinal_number_st_b_in_dom_(U_exp_a)_holds_
(U_exp_a)_._b_=_exp_(a,b)
let b be ordinal number ; ::_thesis: ( b in dom (U exp a) implies (U exp a) . b = exp (a,b) )
assume  b in dom (U exp a) ; ::_thesis: (U exp a) . b = exp (a,b)
then  b in U by A1, ORDINAL1:def_9;
hence  (U exp a) . b = exp (a,b) by Def8; ::_thesis: verum
end;
hence  U exp a is increasing by A3, ORDINAL5:10; :: according to ORDINAL6:def_3 ::_thesis: U exp a is continuous
let b be ordinal number ; :: according to ORDINAL2:def_13 ::_thesis: for b1 being set holds
( not b in dom (U exp a) or b = {} or not b is limit_ordinal or not b1 = (U exp a) . b or b1 is_limes_of (U exp a) | b )
let c be ordinal number ; ::_thesis: ( not b in dom (U exp a) or b = {} or not b is limit_ordinal or not c = (U exp a) . b or c is_limes_of (U exp a) | b )
assume A5: ( b in dom (U exp a) & b <> {} & b is limit_ordinal & c = (U exp a) . b ) ; ::_thesis: c is_limes_of (U exp a) | b
then  b c= dom (U exp a) by ORDINAL1:def_2;
then A6: dom ((U exp a) | b) = b by RELAT_1:62;
A7: (U exp a) | b is increasing by A4, A3, ORDINAL4:15, ORDINAL5:10;
A8: b in U by A1, A5, ORDINAL1:def_9;
then A9: (U exp a) . b = exp (a,b) by Def8;
 (U exp a) . b = Union ((U exp a) | b)
proof
thus  (U exp a) . b c= Union ((U exp a) | b) :: according to XBOOLE_0:def_10 ::_thesis: Union ((U exp a) | b) c= (U exp a) . b
proof
let c be ordinal number ; :: according to ORDINAL1:def_5 ::_thesis: ( not c in (U exp a) . b or c in Union ((U exp a) | b) )
assume  c in (U exp a) . b ; ::_thesis: c in Union ((U exp a) | b)
then consider d being ordinal number  such that
A10: ( d in b & c in exp (a,d) ) by A2, A5, A9, ORDINAL5:11;
 d in U by A8, A10, ORDINAL1:10;
then  exp (a,d) = (U exp a) . d by Def8
.= ((U exp a) | b) . d by A10, FUNCT_1:49 ;
hence  c in Union ((U exp a) | b) by A6, A10, CARD_5:2; ::_thesis: verum
end;
let c be ordinal number ; :: according to ORDINAL1:def_5 ::_thesis: ( not c in Union ((U exp a) | b) or c in (U exp a) . b )
assume  c in Union ((U exp a) | b) ; ::_thesis: c in (U exp a) . b
then consider x being set  such that
A11: ( x in b & c in ((U exp a) | b) . x ) by A6, CARD_5:2;
reconsider x = x as Ordinal by A11;
 x in U by A8, A11, ORDINAL1:10;
then  exp (a,x) = (U exp a) . x by Def8
.= ((U exp a) | b) . x by A11, FUNCT_1:49 ;
hence  c in (U exp a) . b by A2, A11, A5, A9, ORDINAL5:11; ::_thesis: verum
end;
hence  c is_limes_of (U exp a) | b by A5, A7, A6, ORDINAL5:6; ::_thesis: verum
end;
end;

definition
let g be Function;
attrg is Ordinal-Sequence-valued  means :Def9: :: ORDINAL6:def 9
 for x being set st x in rng g holds
x is Ordinal-Sequence;
end;

:: deftheorem Def9 defines Ordinal-Sequence-valued ORDINAL6:def_9_:_
 for g being Function holds
( g is Ordinal-Sequence-valued iff for x being set st x in rng g holds
x is Ordinal-Sequence );

registration
let f be Ordinal-Sequence;
cluster<%f%> ->  Ordinal-Sequence-valued ;
coherence
 <%f%> is Ordinal-Sequence-valued
proof
let x be set ; :: according to ORDINAL6:def_9 ::_thesis: ( x in rng <%f%> implies x is Ordinal-Sequence )
assume  x in rng <%f%> ; ::_thesis: x is Ordinal-Sequence
then  x in {f} by AFINSQ_1:33;
hence  x is Ordinal-Sequence by TARSKI:def_1; ::_thesis: verum
end;
end;

definition
let f be Function;
attrf is with_the_same_dom  means :: ORDINAL6:def 10
 rng f is with_common_domain ;
end;

:: deftheorem  defines with_the_same_dom ORDINAL6:def_10_:_
 for f being Function holds
( f is with_the_same_dom iff rng f is with_common_domain );

registration
let f be Function;
cluster{f} ->  with_common_domain ;
coherence
 {f} is with_common_domain
proof
let g, h be Function; :: according to CARD_3:def_10 ::_thesis: ( not g in {f} or not h in {f} or dom g = dom h )
assume  ( g in {f} & h in {f} ) ; ::_thesis: dom g = dom h
then  ( g = f & h = f ) by TARSKI:def_1;
hence  dom g = dom h ; ::_thesis: verum
end;
end;

registration
let f be Function;
cluster<%f%> ->  with_the_same_dom ;
coherence
 <%f%> is with_the_same_dom
proof
 rng <%f%> = {f} by AFINSQ_1:33;
hence  rng <%f%> is with_common_domain ; :: according to ORDINAL6:def_10 ::_thesis: verum
end;
end;

registration
cluster Relation-like Function-like T-Sequence-like non empty Ordinal-Sequence-valued with_the_same_dom for set ;
existence
 ex b1 being T-Sequence st
( not b1 is empty & b1 is Ordinal-Sequence-valued & b1 is with_the_same_dom )
proof
set f = the Ordinal-Sequence;
take  <% the Ordinal-Sequence%> ; ::_thesis: ( not <% the Ordinal-Sequence%> is empty & <% the Ordinal-Sequence%> is Ordinal-Sequence-valued & <% the Ordinal-Sequence%> is with_the_same_dom )
thus  ( not <% the Ordinal-Sequence%> is empty & <% the Ordinal-Sequence%> is Ordinal-Sequence-valued & <% the Ordinal-Sequence%> is with_the_same_dom ) ; ::_thesis: verum
end;
end;

registration
let g be Ordinal-Sequence-valued Function;
let x be set ;
clusterg . x ->  Relation-like Function-like ;
coherence
 ( g . x is Relation-like & g . x is Function-like )
proof
percases ( g . x = {} or x in dom g ) by FUNCT_1:def_2;
suppose g . x = {} ; ::_thesis: ( g . x is Relation-like & g . x is Function-like )
hence  ( g . x is Relation-like & g . x is Function-like ) ; ::_thesis: verum
end;
suppose x in dom g ; ::_thesis: ( g . x is Relation-like & g . x is Function-like )
then  g . x in rng g by FUNCT_1:def_3;
hence  ( g . x is Relation-like & g . x is Function-like ) by Def9; ::_thesis: verum
end;
end;
end;
end;

registration
let g be Ordinal-Sequence-valued Function;
let x be set ;
clusterg . x ->  T-Sequence-like Ordinal-yielding ;
coherence
 ( g . x is T-Sequence-like & g . x is Ordinal-yielding )
proof
percases ( g . x = {} or x in dom g ) by FUNCT_1:def_2;
suppose g . x = {} ; ::_thesis: ( g . x is T-Sequence-like & g . x is Ordinal-yielding )
hence  ( g . x is T-Sequence-like & g . x is Ordinal-yielding ) ; ::_thesis: verum
end;
suppose x in dom g ; ::_thesis: ( g . x is T-Sequence-like & g . x is Ordinal-yielding )
then  g . x in rng g by FUNCT_1:def_3;
hence  ( g . x is T-Sequence-like & g . x is Ordinal-yielding ) by Def9; ::_thesis: verum
end;
end;
end;
end;

registration
let g be T-Sequence;
let a be ordinal number ;
clusterg | a ->  T-Sequence-like ;
coherence
 g | a is T-Sequence-like ;
end;

registration
let g be Ordinal-Sequence-valued Function;
let X be set ;
clusterg | X ->  Ordinal-Sequence-valued ;
coherence
 g | X is Ordinal-Sequence-valued
proof
let x be set ; :: according to ORDINAL6:def_9 ::_thesis: ( x in rng (g | X) implies x is Ordinal-Sequence )
 rng (g | X) c= rng g by RELAT_1:70;
hence  ( x in rng (g | X) implies x is Ordinal-Sequence ) by Def9; ::_thesis: verum
end;
end;

registration
let a, b be ordinal number ;
cluster Function-like V30(a,b)  ->  T-Sequence-like Ordinal-yielding for Element of bool [:a,b:];
coherence
 for b1 being Function of a,b holds
( b1 is Ordinal-yielding & b1 is T-Sequence-like )
proof
let f be Function of a,b; ::_thesis: ( f is Ordinal-yielding & f is T-Sequence-like )
 rng f c= b by RELAT_1:def_19;
hence  ex c being ordinal number st rng f c= c ; :: according to ORDINAL2:def_4 ::_thesis: f is T-Sequence-like
 ( b = {} implies f = {} ) ;
hence  dom f is ordinal by FUNCT_2:def_1; :: according to ORDINAL1:def_7 ::_thesis: verum
end;
end;

definition
let g be Ordinal-Sequence-valued T-Sequence;
func criticals g ->  Ordinal-Sequence equals :: ORDINAL6:def 11
 numbering  {  a where a is Element of dom (g . 0) : ( a in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) )  }  ;
coherence
 numbering  {  a where a is Element of dom (g . 0) : ( a in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) )  }  is Ordinal-Sequence ;
end;

:: deftheorem  defines criticals ORDINAL6:def_11_:_
 for g being Ordinal-Sequence-valued T-Sequence holds criticals g = numbering  {  a where a is Element of dom (g . 0) : ( a in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) )  }  ;

theorem Th46: :: ORDINAL6:46
for g being Ordinal-Sequence-valued T-Sequence holds  {  a where a is Element of dom (g . 0) : ( a in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) )  }  is ordinal-membered
proof
let g be Ordinal-Sequence-valued T-Sequence; ::_thesis:  {  a where a is Element of dom (g . 0) : ( a in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) )  }  is ordinal-membered
now__::_thesis:_for_x_being_set_st_x_in__{__a_where_a_is_Element_of_dom_(g_._0)_:_(_a_in_dom_(g_._0)_&_(_for_f_being_Ordinal-Sequence_st_f_in_rng_g_holds_
a_is_a_fixpoint_of_f_)_)__}__holds_
x_is_ordinal
let x be set ; ::_thesis: ( x in  {  a where a is Element of dom (g . 0) : ( a in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) )  }  implies x is ordinal )
assume  x in  {  a where a is Element of dom (g . 0) : ( a in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) )  }  ; ::_thesis: x is ordinal
then  ex a being Element of dom (g . 0) st
( x = a & a in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) ) ;
hence  x is ordinal ; ::_thesis: verum
end;
hence   {  a where a is Element of dom (g . 0) : ( a in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) )  }  is ordinal-membered by Th1; ::_thesis: verum
end;

theorem Th47: :: ORDINAL6:47
for a, b being ordinal number
for g being Ordinal-Sequence-valued T-Sequence st a in dom g & b in dom (criticals g) holds
(criticals g) . b is_a_fixpoint_of g . a
proof
let a, b be ordinal number ; ::_thesis: for g being Ordinal-Sequence-valued T-Sequence st a in dom g & b in dom (criticals g) holds
(criticals g) . b is_a_fixpoint_of g . a
let g be Ordinal-Sequence-valued T-Sequence; ::_thesis: ( a in dom g & b in dom (criticals g) implies (criticals g) . b is_a_fixpoint_of g . a )
assume that
A1: a in dom g and
A2: b in dom (criticals g) ; ::_thesis: (criticals g) . b is_a_fixpoint_of g . a
set h = criticals g;
set X =  {  c where c is Element of dom (g . 0) : ( c in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
c is_a_fixpoint_of f ) )  }  ;
  {  c where c is Element of dom (g . 0) : ( c in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
c is_a_fixpoint_of f ) )  }  is ordinal-membered by Th46;
then  rng (criticals g) =  {  c where c is Element of dom (g . 0) : ( c in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
c is_a_fixpoint_of f ) )  }  by Th19;
then  (criticals g) . b in  {  c where c is Element of dom (g . 0) : ( c in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
c is_a_fixpoint_of f ) )  }  by A2, FUNCT_1:def_3;
then consider c being Element of dom (g . 0) such that
A3: ( (criticals g) . b = c & c in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
c is_a_fixpoint_of f ) ) ;
 g . a in rng g by A1, FUNCT_1:def_3;
hence  (criticals g) . b is_a_fixpoint_of g . a by A3; ::_thesis: verum
end;

theorem :: ORDINAL6:48
for x being set
for g being Ordinal-Sequence-valued T-Sequence st x in dom (criticals g) holds
x c= (criticals g) . x by ORDINAL4:10;

theorem Th49: :: ORDINAL6:49
for f being Ordinal-Sequence
for g being Ordinal-Sequence-valued T-Sequence st f in rng g holds
dom (criticals g) c= dom f
proof
let f be Ordinal-Sequence; ::_thesis: for g being Ordinal-Sequence-valued T-Sequence st f in rng g holds
dom (criticals g) c= dom f
let g be Ordinal-Sequence-valued T-Sequence; ::_thesis: ( f in rng g implies dom (criticals g) c= dom f )
assume A1: f in rng g ; ::_thesis: dom (criticals g) c= dom f
let x be Ordinal; :: according to ORDINAL1:def_5 ::_thesis: ( not x in dom (criticals g) or x in dom f )
set X =  {  a where a is Element of dom (g . 0) : ( a in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) )  }  ;
assume A2: x in dom (criticals g) ; ::_thesis: x in dom f
then  (criticals g) . x in rng (criticals g) by FUNCT_1:def_3;
then  ( (criticals g) . x in On  {  a where a is Element of dom (g . 0) : ( a in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) )  }  &  {  a where a is Element of dom (g . 0) : ( a in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) )  }  is ordinal-membered ) by Th18, Th46;
then  (criticals g) . x in  {  a where a is Element of dom (g . 0) : ( a in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) )  }  by Th2;
then consider a being Element of dom (g . 0) such that
A3: ( (criticals g) . x = a & a in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) ) ;
 a is_a_fixpoint_of f by A1, A3;
then  ( x c= a & a in dom f & a = f . a ) by A2, A3, ABIAN:def_3, ORDINAL4:10;
hence  x in dom f by ORDINAL1:12; ::_thesis: verum
end;

theorem Th50: :: ORDINAL6:50
for b being ordinal number
for g being Ordinal-Sequence-valued T-Sequence st dom g <> {} & ( for c being ordinal number st c in dom g holds
b is_a_fixpoint_of g . c ) holds
ex a being ordinal number st
( a in dom (criticals g) & b = (criticals g) . a )
proof
let b be ordinal number ; ::_thesis: for g being Ordinal-Sequence-valued T-Sequence st dom g <> {} & ( for c being ordinal number st c in dom g holds
b is_a_fixpoint_of g . c ) holds
ex a being ordinal number st
( a in dom (criticals g) & b = (criticals g) . a )
let g be Ordinal-Sequence-valued T-Sequence; ::_thesis: ( dom g <> {} & ( for c being ordinal number st c in dom g holds
b is_a_fixpoint_of g . c ) implies ex a being ordinal number st
( a in dom (criticals g) & b = (criticals g) . a ) )
reconsider X =  {  a where a is Element of dom (g . 0) : ( a in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) )  }  as ordinal-membered set by Th46;
assume that
A1: dom g <> {} and
A2: for c being ordinal number st c in dom g holds
b is_a_fixpoint_of g . c ; ::_thesis: ex a being ordinal number st
( a in dom (criticals g) & b = (criticals g) . a )
 b is_a_fixpoint_of g . 0 by A2, A1, ORDINAL3:8;
then A3: b in dom (g . 0) by ABIAN:def_3;
now__::_thesis:_for_f_being_Ordinal-Sequence_st_f_in_rng_g_holds_
b_is_a_fixpoint_of_f
let f be Ordinal-Sequence; ::_thesis: ( f in rng g implies b is_a_fixpoint_of f )
assume  f in rng g ; ::_thesis: b is_a_fixpoint_of f
then  ex x being set st
( x in dom g & f = g . x ) by FUNCT_1:def_3;
hence  b is_a_fixpoint_of f by A2; ::_thesis: verum
end;
then  b in X by A3;
then  b in rng (criticals g) by Th19;
then  ex x being set st
( x in dom (criticals g) & b = (criticals g) . x ) by FUNCT_1:def_3;
hence  ex a being ordinal number st
( a in dom (criticals g) & b = (criticals g) . a ) ; ::_thesis: verum
end;

theorem :: ORDINAL6:51
for a being ordinal number
for l being limit_ordinal non empty Ordinal
for g being Ordinal-Sequence-valued T-Sequence st dom g <> {} & l c= dom (criticals g) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) & ( for x being set st x in l holds
(criticals g) . x in a ) holds
l in dom (criticals g)
proof
let a be ordinal number ; ::_thesis: for l being limit_ordinal non empty Ordinal
for g being Ordinal-Sequence-valued T-Sequence st dom g <> {} & l c= dom (criticals g) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) & ( for x being set st x in l holds
(criticals g) . x in a ) holds
l in dom (criticals g)
let l be limit_ordinal non empty Ordinal; ::_thesis: for g being Ordinal-Sequence-valued T-Sequence st dom g <> {} & l c= dom (criticals g) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) & ( for x being set st x in l holds
(criticals g) . x in a ) holds
l in dom (criticals g)
let g be Ordinal-Sequence-valued T-Sequence; ::_thesis: ( dom g <> {} & l c= dom (criticals g) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) & ( for x being set st x in l holds
(criticals g) . x in a ) implies l in dom (criticals g) )
set h = criticals g;
assume that
A1: dom g <> {} and
A2: l c= dom (criticals g) and
A3: for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f and
A4: for x being set st x in l holds
(criticals g) . x in a ; ::_thesis: l in dom (criticals g)
now__::_thesis:_for_c_being_ordinal_number_st_c_in_dom_g_holds_
a_is_a_fixpoint_of_g_._c
let c be ordinal number ; ::_thesis: ( c in dom g implies a is_a_fixpoint_of g . c )
assume  c in dom g ; ::_thesis: a is_a_fixpoint_of g . c
then  g . c in rng g by FUNCT_1:def_3;
hence  a is_a_fixpoint_of g . c by A3; ::_thesis: verum
end;
then consider b being ordinal number  such that
A5: ( b in dom (criticals g) & a = (criticals g) . b ) by A1, Th50;
 l c= b
proof
let x be Ordinal; :: according to ORDINAL1:def_5 ::_thesis: ( not x in l or x in b )
assume  x in l ; ::_thesis: x in b
then  ( x in dom (criticals g) & (criticals g) . x in (criticals g) . b ) by A2, A4, A5;
hence  x in b by A5, Th23; ::_thesis: verum
end;
hence  l in dom (criticals g) by A5, ORDINAL1:12; ::_thesis: verum
end;

theorem Th52: :: ORDINAL6:52
for l being limit_ordinal non empty Ordinal
for g being Ordinal-Sequence-valued T-Sequence st dom g <> {} & ( for a being ordinal number st a in dom g holds
g . a is normal ) & l in dom (criticals g) holds
(criticals g) . l = Union ((criticals g) | l)
proof
let l be limit_ordinal non empty Ordinal; ::_thesis: for g being Ordinal-Sequence-valued T-Sequence st dom g <> {} & ( for a being ordinal number st a in dom g holds
g . a is normal ) & l in dom (criticals g) holds
(criticals g) . l = Union ((criticals g) | l)
let F be Ordinal-Sequence-valued T-Sequence; ::_thesis: ( dom F <> {} & ( for a being ordinal number st a in dom F holds
F . a is normal ) & l in dom (criticals F) implies (criticals F) . l = Union ((criticals F) | l) )
assume A1: dom F <> {} ; ::_thesis: ( ex a being ordinal number st
( a in dom F & not F . a is normal ) or not l in dom (criticals F) or (criticals F) . l = Union ((criticals F) | l) )
set g = criticals F;
reconsider h = (criticals F) | l as increasing Ordinal-Sequence by ORDINAL4:15;
set X = rng h;
assume A2: ( ( for a being ordinal number st a in dom F holds
F . a is normal ) & l in dom (criticals F) ) ; ::_thesis: (criticals F) . l = Union ((criticals F) | l)
A3: now__::_thesis:_for_a_being_ordinal_number_st_a_in_dom_F_holds_
(_(criticals_F)_._l_in_dom_(F_._a)_&_(F_._a)_._((criticals_F)_._l)_=_(criticals_F)_._l_)
let a be ordinal number ; ::_thesis: ( a in dom F implies ( (criticals F) . l in dom (F . a) & (F . a) . ((criticals F) . l) = (criticals F) . l ) )
set f = F . a;
assume  a in dom F ; ::_thesis: ( (criticals F) . l in dom (F . a) & (F . a) . ((criticals F) . l) = (criticals F) . l )
then  (criticals F) . l is_a_fixpoint_of F . a by A2, Th47;
hence  ( (criticals F) . l in dom (F . a) & (F . a) . ((criticals F) . l) = (criticals F) . l ) by ABIAN:def_3; ::_thesis: verum
end;
A4: l c= dom (criticals F) by A2, ORDINAL1:def_2;
then A5: dom h = l by RELAT_1:62;
A6: for a being ordinal number
for x being set st a in dom F & x in rng h holds
x is_a_fixpoint_of F . a
proof
let a be ordinal number ; ::_thesis: for x being set st a in dom F & x in rng h holds
x is_a_fixpoint_of F . a
let x be set ; ::_thesis: ( a in dom F & x in rng h implies x is_a_fixpoint_of F . a )
assume A7: ( a in dom F & x in rng h ) ; ::_thesis: x is_a_fixpoint_of F . a
then consider y being set  such that
A8: ( y in dom h & x = h . y ) by FUNCT_1:def_3;
 ( x = (criticals F) . y & y in dom (criticals F) ) by A4, A5, A8, FUNCT_1:47;
hence  x is_a_fixpoint_of F . a by A7, Th47; ::_thesis: verum
end;
reconsider u = union (rng h) as Ordinal ;
A9: h <> {} by A5;
now__::_thesis:_for_x_being_set_st_x_in_rng_h_holds_
x_c=_(criticals_F)_._l
let x be set ; ::_thesis: ( x in rng h implies x c= (criticals F) . l )
assume  x in rng h ; ::_thesis: x c= (criticals F) . l
then consider y being set  such that
A10: ( y in dom h & x = h . y ) by FUNCT_1:def_3;
 ( x = (criticals F) . y & y in dom (criticals F) ) by A4, A5, A10, FUNCT_1:47;
then  x in (criticals F) . l by A2, A5, A10, ORDINAL2:def_12;
hence  x c= (criticals F) . l by ORDINAL1:def_2; ::_thesis: verum
end;
then A11: u c= (criticals F) . l by ZFMISC_1:76;
now__::_thesis:_for_c_being_ordinal_number_st_c_in_dom_F_holds_
u_is_a_fixpoint_of_F_._c
let c be ordinal number ; ::_thesis: ( c in dom F implies u is_a_fixpoint_of F . c )
set f = F . c;
assume A12: c in dom F ; ::_thesis: u is_a_fixpoint_of F . c
then A13: (criticals F) . l in dom (F . c) by A3;
then A14: u in dom (F . c) by A11, ORDINAL1:12;
A15: F . c is normal by A2, A12;
 for x being set st x in rng h holds
x is_a_fixpoint_of F . c by A6, A12;
then  u = (F . c) . u by A9, A13, A15, Th37, A11, ORDINAL1:12;
hence  u is_a_fixpoint_of F . c by A14, ABIAN:def_3; ::_thesis: verum
end;
then consider a being ordinal number  such that
A16: ( a in dom (criticals F) & u = (criticals F) . a ) by A1, Th50;
 a = l
proof
thus  a c= l by A2, A16, A11, Th22; :: according to XBOOLE_0:def_10 ::_thesis: l c= a
let x be Ordinal; :: according to ORDINAL1:def_5 ::_thesis: ( not x in l or x in a )
assume A17: x in l ; ::_thesis: x in a
then A18: succ x in l by ORDINAL1:28;
then A19: ( (criticals F) . x = h . x & (criticals F) . (succ x) = h . (succ x) & h . (succ x) in rng h ) by A5, A17, FUNCT_1:47, FUNCT_1:def_3;
 x in succ x by ORDINAL1:6;
then  h . x in h . (succ x) by A5, A18, ORDINAL2:def_12;
then  (criticals F) . x in u by A19, TARSKI:def_4;
then  ( (criticals F) . a c/= (criticals F) . x & x in dom (criticals F) ) by A4, A16, A17, Th4;
then  a c/= x by A16, Th22;
hence  x in a by Th4; ::_thesis: verum
end;
hence  (criticals F) . l = Union ((criticals F) | l) by A16; ::_thesis: verum
end;

theorem Th53: :: ORDINAL6:53
for g being Ordinal-Sequence-valued T-Sequence st dom g <> {} & ( for a being ordinal number st a in dom g holds
g . a is normal ) holds
criticals g is continuous
proof
let g be Ordinal-Sequence-valued T-Sequence; ::_thesis: ( dom g <> {} & ( for a being ordinal number st a in dom g holds
g . a is normal ) implies criticals g is continuous )
assume A1: dom g <> {} ; ::_thesis: ( ex a being ordinal number st
( a in dom g & not g . a is normal ) or criticals g is continuous )
assume A2: for a being ordinal number st a in dom g holds
g . a is normal ; ::_thesis: criticals g is continuous
set f = criticals g;
let a be ordinal number ; :: according to ORDINAL2:def_13 ::_thesis: for b1 being set holds
( not a in dom (criticals g) or a = {} or not a is limit_ordinal or not b1 = (criticals g) . a or b1 is_limes_of (criticals g) | a )
let b be ordinal number ; ::_thesis: ( not a in dom (criticals g) or a = {} or not a is limit_ordinal or not b = (criticals g) . a or b is_limes_of (criticals g) | a )
reconsider h = (criticals g) | a as increasing Ordinal-Sequence by ORDINAL4:15;
assume A3: ( a in dom (criticals g) & a <> {} & a is limit_ordinal & b = (criticals g) . a ) ; ::_thesis: b is_limes_of (criticals g) | a
then A4: b = Union h by A1, A2, Th52;
 a c= dom (criticals g) by A3, ORDINAL1:def_2;
then  dom h = a by RELAT_1:62;
hence  b is_limes_of (criticals g) | a by A3, A4, ORDINAL5:6; ::_thesis: verum
end;

theorem Th54: :: ORDINAL6:54
for g being Ordinal-Sequence-valued T-Sequence st dom g <> {} & ( for a being ordinal number st a in dom g holds
g . a is normal ) holds
for a being ordinal number
for f being Ordinal-Sequence st a in dom (criticals g) & f in rng g holds
f . a c= (criticals g) . a
proof
let F be Ordinal-Sequence-valued T-Sequence; ::_thesis: ( dom F <> {} & ( for a being ordinal number st a in dom F holds
F . a is normal ) implies for a being ordinal number
for f being Ordinal-Sequence st a in dom (criticals F) & f in rng F holds
f . a c= (criticals F) . a )
assume that
A1: dom F <> {} and
A2: for a being ordinal number st a in dom F holds
F . a is normal ; ::_thesis: for a being ordinal number
for f being Ordinal-Sequence st a in dom (criticals F) & f in rng F holds
f . a c= (criticals F) . a
let a be ordinal number ; ::_thesis: for f being Ordinal-Sequence st a in dom (criticals F) & f in rng F holds
f . a c= (criticals F) . a
let f be Ordinal-Sequence; ::_thesis: ( a in dom (criticals F) & f in rng F implies f . a c= (criticals F) . a )
assume that
A3: a in dom (criticals F) and
A4: f in rng F ; ::_thesis: f . a c= (criticals F) . a
consider x being set  such that
A5: ( x in dom F & f = F . x ) by A4, FUNCT_1:def_3;
A6: f is normal by A5, A2;
set g = criticals F;
A7: dom (criticals F) c= dom f by A4, Th49;
defpred S1[ Ordinal] means ( $1 in dom (criticals F) implies f . $1 c= (criticals F) . $1 );
A8: S1[ {} ]
proof
assume  {} in dom (criticals F) ; ::_thesis: f . {} c= (criticals F) . {}
then  (criticals F) . 0 is_a_fixpoint_of f by A5, Th47;
then  ( f . ((criticals F) . 0) = (criticals F) . 0 & (criticals F) . 0 in dom f ) by ABIAN:def_3;
hence  f . {} c= (criticals F) . {} by A6, ORDINAL4:9, XBOOLE_1:2; ::_thesis: verum
end;
A9: for a being ordinal number st S1[a] holds
S1[ succ a]
proof
let a be ordinal number ; ::_thesis: ( S1[a] implies S1[ succ a] )
assume that
 S1[a] and
A10: succ a in dom (criticals F) ; ::_thesis: f . (succ a) c= (criticals F) . (succ a)
 (criticals F) . (succ a) is_a_fixpoint_of f by A5, A10, Th47;
then  ( (criticals F) . (succ a) in dom f & f . ((criticals F) . (succ a)) = (criticals F) . (succ a) ) by ABIAN:def_3;
hence  f . (succ a) c= (criticals F) . (succ a) by A6, A10, ORDINAL4:9, ORDINAL4:10; ::_thesis: verum
end;
A11: for a being ordinal number st a <> {} & a is limit_ordinal & ( for b being ordinal number st b in a holds
S1[b] ) holds
S1[a]
proof
let a be ordinal number ; ::_thesis: ( a <> {} & a is limit_ordinal & ( for b being ordinal number st b in a holds
S1[b] ) implies S1[a] )
assume that
A12: ( a <> {} & a is limit_ordinal ) and
A13: for b being ordinal number st b in a holds
S1[b] and
A14: a in dom (criticals F) ; ::_thesis: f . a c= (criticals F) . a
 criticals F is continuous by A1, A2, Th53;
then  ( f . a is_limes_of f | a & (criticals F) . a is_limes_of (criticals F) | a ) by A6, A7, A12, A14, ORDINAL2:def_13;
then A15: ( f . a = lim (f | a) & (criticals F) . a = lim ((criticals F) | a) ) by ORDINAL2:def_10;
A16: ( f | a is increasing & (criticals F) | a is increasing ) by A6, ORDINAL4:15;
A17: ( a c= dom f & a c= dom (criticals F) ) by A7, A14, ORDINAL1:def_2;
then A18: ( dom (f | a) = a & dom ((criticals F) | a) = a ) by RELAT_1:62;
then  ( Union (f | a) is_limes_of f | a & Union ((criticals F) | a) is_limes_of (criticals F) | a ) by A12, A16, ORDINAL5:6;
then A19: ( f . a = Union (f | a) & (criticals F) . a = Union ((criticals F) | a) ) by A15, ORDINAL2:def_10;
let b be ordinal number ; :: according to ORDINAL1:def_5 ::_thesis: ( not b in f . a or b in (criticals F) . a )
assume  b in f . a ; ::_thesis: b in (criticals F) . a
then consider x being set  such that
A20: ( x in a & b in (f | a) . x ) by A18, A19, CARD_5:2;
 ( (f | a) . x = f . x & ((criticals F) | a) . x = (criticals F) . x & f . x c= (criticals F) . x ) by A17, A13, A20, FUNCT_1:49;
hence  b in (criticals F) . a by A20, A18, A19, CARD_5:2; ::_thesis: verum
end;
 for a being ordinal number holds S1[a] from ORDINAL2:sch_1(A8, A9, A11);
hence  f . a c= (criticals F) . a by A3; ::_thesis: verum
end;

theorem Th55: :: ORDINAL6:55
for g1, g2 being Ordinal-Sequence-valued T-Sequence st dom g1 = dom g2 & dom g1 <> {} & ( for a being ordinal number st a in dom g1 holds
g1 . a c= g2 . a ) holds
criticals g1 c= criticals g2
proof
let g1, g2 be Ordinal-Sequence-valued T-Sequence; ::_thesis: ( dom g1 = dom g2 & dom g1 <> {} & ( for a being ordinal number st a in dom g1 holds
g1 . a c= g2 . a ) implies criticals g1 c= criticals g2 )
assume A1: dom g1 = dom g2 ; ::_thesis: ( not dom g1 <> {} or ex a being ordinal number st
( a in dom g1 & not g1 . a c= g2 . a ) or criticals g1 c= criticals g2 )
assume A2: dom g1 <> {} ; ::_thesis: ( ex a being ordinal number st
( a in dom g1 & not g1 . a c= g2 . a ) or criticals g1 c= criticals g2 )
assume A3: for a being ordinal number st a in dom g1 holds
g1 . a c= g2 . a ; ::_thesis: criticals g1 c= criticals g2
set f1 = g1 . 0;
set f2 = g2 . 0;
 0 in dom g1 by A2, ORDINAL3:8;
then  ( g1 . 0 c= g2 . 0 & g1 . 0 in rng g1 & g2 . 0 in rng g2 ) by A1, A3, FUNCT_1:def_3;
then A4: dom (g1 . 0) c= dom (g2 . 0) by GRFUNC_1:2;
set X =  {  a where a is Element of dom (g1 . 0) : ( a in dom (g1 . 0) & ( for f being Ordinal-Sequence st f in rng g1 holds
a is_a_fixpoint_of f ) )  }  ;
set Z =  {  a where a is Element of dom (g2 . 0) : ( a in dom (g2 . 0) & ( for f being Ordinal-Sequence st f in rng g2 holds
a is_a_fixpoint_of f ) )  }  ;
reconsider X =  {  a where a is Element of dom (g1 . 0) : ( a in dom (g1 . 0) & ( for f being Ordinal-Sequence st f in rng g1 holds
a is_a_fixpoint_of f ) )  }  , Z =  {  a where a is Element of dom (g2 . 0) : ( a in dom (g2 . 0) & ( for f being Ordinal-Sequence st f in rng g2 holds
a is_a_fixpoint_of f ) )  }  as ordinal-membered set by Th46;
set Y = Z \ X;
A5: now__::_thesis:_for_x,_y_being_set_st_x_in_X_&_y_in_Z_\_X_holds_
x_in_y
let x, y be set ; ::_thesis: ( x in X & y in Z \ X implies x in y )
assume  x in X ; ::_thesis: ( y in Z \ X implies x in y )
then consider a being Element of dom (g1 . 0) such that
A6: ( x = a & a in dom (g1 . 0) & ( for f being Ordinal-Sequence st f in rng g1 holds
a is_a_fixpoint_of f ) ) ;
assume  y in Z \ X ; ::_thesis: x in y
then A7: ( y in Z & not y in X ) by XBOOLE_0:def_5;
then consider b being Element of dom (g2 . 0) such that
A8: ( y = b & b in dom (g2 . 0) & ( for f being Ordinal-Sequence st f in rng g2 holds
b is_a_fixpoint_of f ) ) ;
assume  not x in y ; ::_thesis: contradiction
then A9: b c= a by A6, A8, ORDINAL1:16;
then A10: b in dom (g1 . 0) by A6, ORDINAL1:12;
now__::_thesis:_for_f_being_Ordinal-Sequence_st_f_in_rng_g1_holds_
b_is_a_fixpoint_of_f
let f be Ordinal-Sequence; ::_thesis: ( f in rng g1 implies b is_a_fixpoint_of f )
assume A11: f in rng g1 ; ::_thesis: b is_a_fixpoint_of f
then consider z being set  such that
A12: ( z in dom g1 & f = g1 . z ) by FUNCT_1:def_3;
A13: f c= g2 . z by A3, A12;
 g2 . z in rng g2 by A1, A12, FUNCT_1:def_3;
then A14: b is_a_fixpoint_of g2 . z by A8;
 a is_a_fixpoint_of f by A6, A11;
then  a in dom f by ABIAN:def_3;
then A15: b in dom f by A9, ORDINAL1:12;
then f . b = (g2 . z) . b by A13, GRFUNC_1:2
.= b by A14, ABIAN:def_3 ;
hence  b is_a_fixpoint_of f by A15, ABIAN:def_3; ::_thesis: verum
end;
hence  contradiction by A7, A8, A10; ::_thesis: verum
end;
 X c= Z
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Z )
assume  x in X ; ::_thesis: x in Z
then consider a being Element of dom (g1 . 0) such that
A16: ( x = a & a in dom (g1 . 0) & ( for f being Ordinal-Sequence st f in rng g1 holds
a is_a_fixpoint_of f ) ) ;
now__::_thesis:_for_f_being_Ordinal-Sequence_st_f_in_rng_g2_holds_
a_is_a_fixpoint_of_f
let f be Ordinal-Sequence; ::_thesis: ( f in rng g2 implies a is_a_fixpoint_of f )
assume  f in rng g2 ; ::_thesis: a is_a_fixpoint_of f
then consider z being set  such that
A17: ( z in dom g2 & f = g2 . z ) by FUNCT_1:def_3;
A18: g1 . z c= f by A1, A3, A17;
then A19: dom (g1 . z) c= dom f by GRFUNC_1:2;
 g1 . z in rng g1 by A1, A17, FUNCT_1:def_3;
then  a is_a_fixpoint_of g1 . z by A16;
then  ( a in dom (g1 . z) & a = (g1 . z) . a ) by ABIAN:def_3;
then  ( a in dom f & a = f . a ) by A18, A19, GRFUNC_1:2;
hence  a is_a_fixpoint_of f by ABIAN:def_3; ::_thesis: verum
end;
hence  x in Z by A16, A4; ::_thesis: verum
end;
then  X \/ (Z \ X) = Z by XBOOLE_1:45;
then  criticals g2 = (criticals g1) ^ (numbering (Z \ X)) by A5, Th25;
hence  criticals g1 c= criticals g2 by Th9; ::_thesis: verum
end;

definition
let g be Ordinal-Sequence-valued T-Sequence;
func lims g ->  Ordinal-Sequence means :Def12: :: ORDINAL6:def 12
( dom it = dom (g . 0) & ( for a being ordinal number st a in dom it holds
it . a = union  {  ((g . b) . a) where b is Element of dom g : b in dom g  }  ) );
existence
 ex b1 being Ordinal-Sequence st
( dom b1 = dom (g . 0) & ( for a being ordinal number st a in dom b1 holds
b1 . a = union  {  ((g . b) . a) where b is Element of dom g : b in dom g  }  ) )
proof
deffunc H1( Ordinal) ->  set =  {  ((g . b) . $1) where b is Element of dom g : b in dom g  }  ;
deffunc H2( Ordinal) ->  set = union (On H1($1));
consider f being Ordinal-Sequence such that
A1: ( dom f = dom (g . 0) & ( for a being ordinal number st a in dom (g . 0) holds
f . a = H2(a) ) ) from ORDINAL2:sch_3();
take  f ; ::_thesis: ( dom f = dom (g . 0) & ( for a being ordinal number st a in dom f holds
f . a = union  {  ((g . b) . a) where b is Element of dom g : b in dom g  }  ) )
thus  dom f = dom (g . 0) by A1; ::_thesis: for a being ordinal number st a in dom f holds
f . a = union  {  ((g . b) . a) where b is Element of dom g : b in dom g  }
let a be ordinal number ; ::_thesis: ( a in dom f implies f . a = union  {  ((g . b) . a) where b is Element of dom g : b in dom g  }  )
assume  a in dom f ; ::_thesis: f . a = union  {  ((g . b) . a) where b is Element of dom g : b in dom g  }
then A2: f . a = H2(a) by A1;
now__::_thesis:_for_x_being_set_st_x_in_H1(a)_holds_
x_is_ordinal
let x be set ; ::_thesis: ( x in H1(a) implies x is ordinal )
assume  x in H1(a) ; ::_thesis: x is ordinal
then  ex b being Element of dom g st
( x = (g . b) . a & b in dom g ) ;
hence  x is ordinal ; ::_thesis: verum
end;
then  H1(a) is ordinal-membered by Th1;
hence  f . a = union  {  ((g . b) . a) where b is Element of dom g : b in dom g  }  by A2, Th2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Ordinal-Sequence st dom b1 = dom (g . 0) & ( for a being ordinal number st a in dom b1 holds
b1 . a = union  {  ((g . b) . a) where b is Element of dom g : b in dom g  }  ) & dom b2 = dom (g . 0) & ( for a being ordinal number st a in dom b2 holds
b2 . a = union  {  ((g . b) . a) where b is Element of dom g : b in dom g  }  ) holds
b1 = b2
proof
let f1, f2 be Ordinal-Sequence; ::_thesis: ( dom f1 = dom (g . 0) & ( for a being ordinal number st a in dom f1 holds
f1 . a = union  {  ((g . b) . a) where b is Element of dom g : b in dom g  }  ) & dom f2 = dom (g . 0) & ( for a being ordinal number st a in dom f2 holds
f2 . a = union  {  ((g . b) . a) where b is Element of dom g : b in dom g  }  ) implies f1 = f2 )
assume that
A3: ( dom f1 = dom (g . 0) & ( for a being ordinal number st a in dom f1 holds
f1 . a = union  {  ((g . b) . a) where b is Element of dom g : b in dom g  }  ) ) and
A4: ( dom f2 = dom (g . 0) & ( for a being ordinal number st a in dom f2 holds
f2 . a = union  {  ((g . b) . a) where b is Element of dom g : b in dom g  }  ) ) ; ::_thesis: f1 = f2
thus  dom f1 = dom f2 by A3, A4; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds
( not b1 in dom f1 or f1 . b1 = f2 . b1 )
let x be set ; ::_thesis: ( not x in dom f1 or f1 . x = f2 . x )
assume A5: x in dom f1 ; ::_thesis: f1 . x = f2 . x
then  f1 . x = union  {  ((g . b) . x) where b is Element of dom g : b in dom g  }  by A3;
hence  f1 . x = f2 . x by A3, A4, A5; ::_thesis: verum
end;
end;

:: deftheorem Def12 defines lims ORDINAL6:def_12_:_
 for g being Ordinal-Sequence-valued T-Sequence
for b2 being Ordinal-Sequence holds
( b2 = lims g iff ( dom b2 = dom (g . 0) & ( for a being ordinal number st a in dom b2 holds
b2 . a = union  {  ((g . b) . a) where b is Element of dom g : b in dom g  }  ) ) );

theorem Th56: :: ORDINAL6:56
for U being Universe
for g being Ordinal-Sequence-valued T-Sequence st dom g <> {} & dom g in U & ( for a being ordinal number st a in dom g holds
g . a is Ordinal-Sequence of U ) holds
lims g is Ordinal-Sequence of U
proof
let U be Universe; ::_thesis: for g being Ordinal-Sequence-valued T-Sequence st dom g <> {} & dom g in U & ( for a being ordinal number st a in dom g holds
g . a is Ordinal-Sequence of U ) holds
lims g is Ordinal-Sequence of U
let g be Ordinal-Sequence-valued T-Sequence; ::_thesis: ( dom g <> {} & dom g in U & ( for a being ordinal number st a in dom g holds
g . a is Ordinal-Sequence of U ) implies lims g is Ordinal-Sequence of U )
assume A1: ( dom g <> {} & dom g in U ) ; ::_thesis: ( ex a being ordinal number st
( a in dom g & g . a is not Ordinal-Sequence of U ) or lims g is Ordinal-Sequence of U )
assume A2: for a being ordinal number st a in dom g holds
g . a is Ordinal-Sequence of U ; ::_thesis: lims g is Ordinal-Sequence of U
reconsider g0 = g . 0 as Ordinal-Sequence of U by A2, A1, ORDINAL3:8;
A3: dom (lims g) = dom g0 by Def12
.= On U by FUNCT_2:def_1 ;
 rng (lims g) c= On U
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (lims g) or x in On U )
assume  x in rng (lims g) ; ::_thesis: x in On U
then consider y being set  such that
A4: ( y in dom (lims g) & x = (lims g) . y ) by FUNCT_1:def_3;
reconsider y = y as Ordinal by A4;
set X =  {  ((g . b) . y) where b is Element of dom g : b in dom g  }  ;
A5: x = union  {  ((g . b) . y) where b is Element of dom g : b in dom g  }  by A4, Def12;
reconsider a = dom g as non empty Ordinal of U by A1;
deffunc H1( set ) ->  set = (g . $1) . y;
A6: card  {  H1(b) where b is Element of a : b in a  }  c= card a from TREES_2:sch_2();
 card a c= a by CARD_1:8;
then  card  {  ((g . b) . y) where b is Element of dom g : b in dom g  }  c= a by A6, XBOOLE_1:1;
then  card  {  ((g . b) . y) where b is Element of dom g : b in dom g  }  in U by CLASSES1:def_1;
then  card  {  ((g . b) . y) where b is Element of dom g : b in dom g  }  in On U by ORDINAL1:def_9;
then A7: card  {  ((g . b) . y) where b is Element of dom g : b in dom g  }  in card U by CLASSES2:9;
A8:  {  ((g . b) . y) where b is Element of dom g : b in dom g  }  c= On U
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  ((g . b) . y) where b is Element of dom g : b in dom g  }  or z in On U )
assume  z in  {  ((g . b) . y) where b is Element of dom g : b in dom g  }  ; ::_thesis: z in On U
then consider b being Element of a such that
A9: ( z = (g . b) . y & b in a ) ;
reconsider f = g . b as Ordinal-Sequence of U by A2;
 z = f . y by A9;
hence  z in On U by ORDINAL1:def_9; ::_thesis: verum
end;
then reconsider u = union  {  ((g . b) . y) where b is Element of dom g : b in dom g  }  as Ordinal by ORDINAL3:4;
 On U c= U by ORDINAL2:7;
then   {  ((g . b) . y) where b is Element of dom g : b in dom g  }  c= U by A8, XBOOLE_1:1;
then   {  ((g . b) . y) where b is Element of dom g : b in dom g  }  in U by A7, CLASSES1:1;
then  u in U by CLASSES2:59;
hence  x in On U by A5, ORDINAL1:def_9; ::_thesis: verum
end;
hence  lims g is Ordinal-Sequence of U by A3, FUNCT_2:2; ::_thesis: verum
end;

begin

definition
let x be set ;
func OS@ x ->  Ordinal-Sequence equals :Def13: :: ORDINAL6:def 13
x if x is Ordinal-Sequence
otherwise  the Ordinal-Sequence;
correctness
coherence
( ( x is Ordinal-Sequence implies x is Ordinal-Sequence ) & ( x is not Ordinal-Sequence implies the Ordinal-Sequence is Ordinal-Sequence ) );
consistency
for b1 being Ordinal-Sequence holds verum;
;
func OSV@ x ->  Ordinal-Sequence-valued T-Sequence equals :Def14: :: ORDINAL6:def 14
x if x is Ordinal-Sequence-valued T-Sequence
otherwise  the Ordinal-Sequence-valued T-Sequence;
correctness
coherence
( ( x is Ordinal-Sequence-valued T-Sequence implies x is Ordinal-Sequence-valued T-Sequence ) & ( x is not Ordinal-Sequence-valued T-Sequence implies the Ordinal-Sequence-valued T-Sequence is Ordinal-Sequence-valued T-Sequence ) );
consistency
for b1 being Ordinal-Sequence-valued T-Sequence holds verum;
;
end;

:: deftheorem Def13 defines OS@ ORDINAL6:def_13_:_
 for x being set holds
( ( x is Ordinal-Sequence implies OS@ x = x ) & ( x is not Ordinal-Sequence implies OS@ x = the Ordinal-Sequence ) );

:: deftheorem Def14 defines OSV@ ORDINAL6:def_14_:_
 for x being set holds
( ( x is Ordinal-Sequence-valued T-Sequence implies OSV@ x = x ) & ( x is not Ordinal-Sequence-valued T-Sequence implies OSV@ x = the Ordinal-Sequence-valued T-Sequence ) );

definition
let U be Universe;
funcU -Veblen  ->  Ordinal-Sequence-valued T-Sequence means :Def15: :: ORDINAL6:def 15
( dom it = On U & it . 0 = U exp omega & ( for b being ordinal number st succ b in On U holds
it . (succ b) = criticals (it . b) ) & ( for l being limit_ordinal non empty Ordinal st l in On U holds
it . l = criticals (it | l) ) );
existence
 ex b1 being Ordinal-Sequence-valued T-Sequence st
( dom b1 = On U & b1 . 0 = U exp omega & ( for b being ordinal number st succ b in On U holds
b1 . (succ b) = criticals (b1 . b) ) & ( for l being limit_ordinal non empty Ordinal st l in On U holds
b1 . l = criticals (b1 | l) ) )
proof
reconsider o = omega as non trivial Ordinal ;
deffunc H1( set , set ) ->  Ordinal-Sequence = criticals (OS@ $2);
deffunc H2( set , set ) ->  Ordinal-Sequence = criticals (OSV@ $2);
consider L being T-Sequence such that
A1: dom L = On U and
A2: ( {} in On U implies L . {} = U exp o ) and
A3: for b being ordinal number st succ b in On U holds
L . (succ b) = H1(b,L . b) and
A4: for b being ordinal number st b in On U & b <> {} & b is limit_ordinal holds
L . b = H2(b,L | b) from ORDINAL2:sch_5();
defpred S1[ Ordinal] means ( $1 in On U implies L . $1 is Ordinal-Sequence );
A5: S1[ {} ] by A2;
A6: for b being ordinal number st S1[b] holds
S1[ succ b]
proof
let b be ordinal number ; ::_thesis: ( S1[b] implies S1[ succ b] )
assume that
A7: S1[b] and
A8: succ b in On U ; ::_thesis: L . (succ b) is Ordinal-Sequence
 b in succ b by ORDINAL1:6;
then reconsider f = L . b as Ordinal-Sequence by A7, A8, ORDINAL1:10;
L . (succ b) = H1(b,f) by A3, A8
.= criticals f by Def13 ;
hence  L . (succ b) is Ordinal-Sequence ; ::_thesis: verum
end;
A9: for b being ordinal number st b <> {} & b is limit_ordinal & ( for c being ordinal number st c in b holds
S1[c] ) holds
S1[b]
proof
let b be ordinal number ; ::_thesis: ( b <> {} & b is limit_ordinal & ( for c being ordinal number st c in b holds
S1[c] ) implies S1[b] )
assume that
A10: ( b <> {} & b is limit_ordinal ) and
 for c being ordinal number st c in b holds
S1[c] and
A11: b in On U ; ::_thesis: L . b is Ordinal-Sequence
 L . b = H2(b,L | b) by A4, A10, A11;
hence  L . b is Ordinal-Sequence ; ::_thesis: verum
end;
A12: for b being ordinal number holds S1[b] from ORDINAL2:sch_1(A5, A6, A9);
 L is Ordinal-Sequence-valued
proof
let x be set ; :: according to ORDINAL6:def_9 ::_thesis: ( x in rng L implies x is Ordinal-Sequence )
assume  x in rng L ; ::_thesis: x is Ordinal-Sequence
then  ex y being set st
( y in dom L & x = L . y ) by FUNCT_1:def_3;
hence  x is Ordinal-Sequence by A1, A12; ::_thesis: verum
end;
then reconsider L = L as Ordinal-Sequence-valued T-Sequence ;
take  L ; ::_thesis: ( dom L = On U & L . 0 = U exp omega & ( for b being ordinal number st succ b in On U holds
L . (succ b) = criticals (L . b) ) & ( for l being limit_ordinal non empty Ordinal st l in On U holds
L . l = criticals (L | l) ) )
 0-element_of U in On U by ORDINAL1:def_9;
hence  ( dom L = On U & L . 0 = U exp omega ) by A1, A2; ::_thesis: ( ( for b being ordinal number st succ b in On U holds
L . (succ b) = criticals (L . b) ) & ( for l being limit_ordinal non empty Ordinal st l in On U holds
L . l = criticals (L | l) ) )
hereby  ::_thesis: for l being limit_ordinal non empty Ordinal st l in On U holds
L . l = criticals (L | l)
let b be ordinal number ; ::_thesis: ( succ b in On U implies L . (succ b) = criticals (L . b) )
assume A13: succ b in On U ; ::_thesis: L . (succ b) = criticals (L . b)
reconsider f = L . b as Ordinal-Sequence ;
thus L . (succ b) = H1(b,f) by A13, A3
.= criticals (L . b) by Def13 ; ::_thesis: verum
end;
let l be limit_ordinal non empty Ordinal; ::_thesis: ( l in On U implies L . l = criticals (L | l) )
assume  l in On U ; ::_thesis: L . l = criticals (L | l)
hence L . l = H2(l,L | l) by A4
.= criticals (L | l) by Def14 ;
::_thesis: verum
end;
uniqueness
 for b1, b2 being Ordinal-Sequence-valued T-Sequence st dom b1 = On U & b1 . 0 = U exp omega & ( for b being ordinal number st succ b in On U holds
b1 . (succ b) = criticals (b1 . b) ) & ( for l being limit_ordinal non empty Ordinal st l in On U holds
b1 . l = criticals (b1 | l) ) & dom b2 = On U & b2 . 0 = U exp omega & ( for b being ordinal number st succ b in On U holds
b2 . (succ b) = criticals (b2 . b) ) & ( for l being limit_ordinal non empty Ordinal st l in On U holds
b2 . l = criticals (b2 | l) ) holds
b1 = b2
proof
let g1, g2 be Ordinal-Sequence-valued T-Sequence; ::_thesis: ( dom g1 = On U & g1 . 0 = U exp omega & ( for b being ordinal number st succ b in On U holds
g1 . (succ b) = criticals (g1 . b) ) & ( for l being limit_ordinal non empty Ordinal st l in On U holds
g1 . l = criticals (g1 | l) ) & dom g2 = On U & g2 . 0 = U exp omega & ( for b being ordinal number st succ b in On U holds
g2 . (succ b) = criticals (g2 . b) ) & ( for l being limit_ordinal non empty Ordinal st l in On U holds
g2 . l = criticals (g2 | l) ) implies g1 = g2 )
assume that
A14: dom g1 = On U and
A15: g1 . 0 = U exp omega and
A16: for b being ordinal number st succ b in On U holds
g1 . (succ b) = criticals (g1 . b) and
A17: for l being limit_ordinal non empty Ordinal st l in On U holds
g1 . l = criticals (g1 | l) and
A18: dom g2 = On U and
A19: g2 . 0 = U exp omega and
A20: for b being ordinal number st succ b in On U holds
g2 . (succ b) = criticals (g2 . b) and
A21: for l being limit_ordinal non empty Ordinal st l in On U holds
g2 . l = criticals (g2 | l) ; ::_thesis: g1 = g2
deffunc H1( set , Ordinal-Sequence) ->  Ordinal-Sequence = criticals $2;
deffunc H2( set , Ordinal-Sequence-valued T-Sequence) ->  Ordinal-Sequence = criticals $2;
A22: ( {} in On U implies g1 . {} = U exp omega ) by A15;
A23: for b being ordinal number st succ b in On U holds
g1 . (succ b) = H1(b,g1 . b) by A16;
A24: for a being ordinal number st a in On U & a <> {} & a is limit_ordinal holds
g1 . a = H2(a,g1 | a) by A17;
A25: ( {} in On U implies g2 . {} = U exp omega ) by A19;
A26: for b being ordinal number st succ b in On U holds
g2 . (succ b) = H1(b,g2 . b) by A20;
A27: for a being ordinal number st a in On U & a <> {} & a is limit_ordinal holds
g2 . a = H2(a,g2 | a) by A21;
thus  g1 = g2 from ORDINAL2:sch_4(A14, A22, A23, A24, A18, A25, A26, A27); ::_thesis: verum
end;
end;

:: deftheorem Def15 defines -Veblen ORDINAL6:def_15_:_
 for U being Universe
for b2 being Ordinal-Sequence-valued T-Sequence holds
( b2 = U -Veblen iff ( dom b2 = On U & b2 . 0 = U exp omega & ( for b being ordinal number st succ b in On U holds
b2 . (succ b) = criticals (b2 . b) ) & ( for l being limit_ordinal non empty Ordinal st l in On U holds
b2 . l = criticals (b2 | l) ) ) );

registration
cluster epsilon-transitive non empty subset-closed Tarski uncountable universal for set ;
existence
 ex b1 being Universe st b1 is uncountable
proof
take U = Tarski-Class omega; ::_thesis: U is uncountable
 omega in U by CLASSES1:2;
then  card omega in card U by CLASSES2:1;
hence  card U c/= omega ; :: according to CARD_3:def_14 ::_thesis: verum
end;
end;

theorem Th57: :: ORDINAL6:57
for U being Universe holds
( U is uncountable iff omega in U )
proof
let U be Universe; ::_thesis: ( U is uncountable iff omega in U )
thus  ( U is uncountable implies omega in U ) ::_thesis: ( omega in U implies U is uncountable )
proof
assume  card U c/= omega ; :: according to CARD_3:def_14 ::_thesis: omega in U
then  omega in card U by Th4;
then  omega in On U by CLASSES2:9;
hence  omega in U by ORDINAL1:def_9; ::_thesis: verum
end;
assume  omega in U ; ::_thesis: U is uncountable
then  card omega in card U by CLASSES2:1;
hence  card U c/= omega ; :: according to CARD_3:def_14 ::_thesis: verum
end;

theorem Th58: :: ORDINAL6:58
for a, b, c being ordinal number
for U being Universe st a in b & b in U & omega in U & c in dom ((U -Veblen) . b) holds
((U -Veblen) . b) . c is_a_fixpoint_of (U -Veblen) . a
proof
let a, b, c be ordinal number ; ::_thesis: for U being Universe st a in b & b in U & omega in U & c in dom ((U -Veblen) . b) holds
((U -Veblen) . b) . c is_a_fixpoint_of (U -Veblen) . a
let U be Universe; ::_thesis: ( a in b & b in U & omega in U & c in dom ((U -Veblen) . b) implies ((U -Veblen) . b) . c is_a_fixpoint_of (U -Veblen) . a )
assume A1: ( a in b & b in U & omega in U ) ; ::_thesis: ( not c in dom ((U -Veblen) . b) or ((U -Veblen) . b) . c is_a_fixpoint_of (U -Veblen) . a )
set F = U -Veblen ;
defpred S1[ Ordinal] means ( $1 in U implies for a, c being ordinal number st a in $1 & c in dom ((U -Veblen) . $1) holds
((U -Veblen) . $1) . c is_a_fixpoint_of (U -Veblen) . a );
A2: S1[ 0 ] ;
A3: for b being ordinal number st S1[b] holds
S1[ succ b]
proof
let b be ordinal number ; ::_thesis: ( S1[b] implies S1[ succ b] )
assume that
A4: S1[b] and
A5: succ b in U ; ::_thesis: for a, c being ordinal number st a in succ b & c in dom ((U -Veblen) . (succ b)) holds
((U -Veblen) . (succ b)) . c is_a_fixpoint_of (U -Veblen) . a
A6: b in succ b by ORDINAL1:6;
let a, c be ordinal number ; ::_thesis: ( a in succ b & c in dom ((U -Veblen) . (succ b)) implies ((U -Veblen) . (succ b)) . c is_a_fixpoint_of (U -Veblen) . a )
assume  a in succ b ; ::_thesis: ( not c in dom ((U -Veblen) . (succ b)) or ((U -Veblen) . (succ b)) . c is_a_fixpoint_of (U -Veblen) . a )
then A7: ( a in b or a in {b} ) by XBOOLE_0:def_3;
 succ b in On U by A5, ORDINAL1:def_9;
then A8: (U -Veblen) . (succ b) = criticals ((U -Veblen) . b) by Def15;
assume  c in dom ((U -Veblen) . (succ b)) ; ::_thesis: ((U -Veblen) . (succ b)) . c is_a_fixpoint_of (U -Veblen) . a
then A9: ((U -Veblen) . (succ b)) . c is_a_fixpoint_of (U -Veblen) . b by A8, Th29;
then  ( ((U -Veblen) . (succ b)) . c in dom ((U -Veblen) . b) & ((U -Veblen) . (succ b)) . c = ((U -Veblen) . b) . (((U -Veblen) . (succ b)) . c) ) by ABIAN:def_3;
hence  ((U -Veblen) . (succ b)) . c is_a_fixpoint_of (U -Veblen) . a by A4, A5, A6, A7, A9, ORDINAL1:10, TARSKI:def_1; ::_thesis: verum
end;
A10: dom (U -Veblen) = On U by Def15;
A11: for b being ordinal number st b <> {} & b is limit_ordinal & ( for d being ordinal number st d in b holds
S1[d] ) holds
S1[b]
proof
let b be ordinal number ; ::_thesis: ( b <> {} & b is limit_ordinal & ( for d being ordinal number st d in b holds
S1[d] ) implies S1[b] )
assume that
A12: ( b <> {} & b is limit_ordinal ) and
 for d being ordinal number st d in b holds
S1[d] and
A13: b in U ; ::_thesis: for a, c being ordinal number st a in b & c in dom ((U -Veblen) . b) holds
((U -Veblen) . b) . c is_a_fixpoint_of (U -Veblen) . a
A14: b in On U by A13, ORDINAL1:def_9;
then A15: (U -Veblen) . b = criticals ((U -Veblen) | b) by A12, Def15;
 b c= On U by A14, ORDINAL1:def_2;
then A16: dom ((U -Veblen) | b) = b by A10, RELAT_1:62;
let a, c be ordinal number ; ::_thesis: ( a in b & c in dom ((U -Veblen) . b) implies ((U -Veblen) . b) . c is_a_fixpoint_of (U -Veblen) . a )
assume A17: a in b ; ::_thesis: ( not c in dom ((U -Veblen) . b) or ((U -Veblen) . b) . c is_a_fixpoint_of (U -Veblen) . a )
then A18: (U -Veblen) . a = ((U -Veblen) | b) . a by FUNCT_1:49;
set g = (U -Veblen) | b;
set X =  {  z where z is Element of dom (((U -Veblen) | b) . 0) : ( z in dom (((U -Veblen) | b) . 0) & ( for f being Ordinal-Sequence st f in rng ((U -Veblen) | b) holds
z is_a_fixpoint_of f ) )  }  ;
now__::_thesis:_for_x_being_set_st_x_in__{__z_where_z_is_Element_of_dom_(((U_-Veblen)_|_b)_._0)_:_(_z_in_dom_(((U_-Veblen)_|_b)_._0)_&_(_for_f_being_Ordinal-Sequence_st_f_in_rng_((U_-Veblen)_|_b)_holds_
z_is_a_fixpoint_of_f_)_)__}__holds_
x_is_ordinal
let x be set ; ::_thesis: ( x in  {  z where z is Element of dom (((U -Veblen) | b) . 0) : ( z in dom (((U -Veblen) | b) . 0) & ( for f being Ordinal-Sequence st f in rng ((U -Veblen) | b) holds
z is_a_fixpoint_of f ) )  }  implies x is ordinal )
assume  x in  {  z where z is Element of dom (((U -Veblen) | b) . 0) : ( z in dom (((U -Veblen) | b) . 0) & ( for f being Ordinal-Sequence st f in rng ((U -Veblen) | b) holds
z is_a_fixpoint_of f ) )  }  ; ::_thesis: x is ordinal
then  ex a being Element of dom (((U -Veblen) | b) . 0) st
( x = a & a in dom (((U -Veblen) | b) . 0) & ( for f being Ordinal-Sequence st f in rng ((U -Veblen) | b) holds
a is_a_fixpoint_of f ) ) ;
hence  x is ordinal ; ::_thesis: verum
end;
then reconsider X =  {  z where z is Element of dom (((U -Veblen) | b) . 0) : ( z in dom (((U -Veblen) | b) . 0) & ( for f being Ordinal-Sequence st f in rng ((U -Veblen) | b) holds
z is_a_fixpoint_of f ) )  }  as ordinal-membered set by Th1;
assume  c in dom ((U -Veblen) . b) ; ::_thesis: ((U -Veblen) . b) . c is_a_fixpoint_of (U -Veblen) . a
then  ((U -Veblen) . b) . c in rng ((U -Veblen) . b) by FUNCT_1:def_3;
then  ((U -Veblen) . b) . c in X by A15, Th19;
then consider z being Element of dom (((U -Veblen) | b) . 0) such that
A19: ( ((U -Veblen) . b) . c = z & z in dom (((U -Veblen) | b) . 0) & ( for f being Ordinal-Sequence st f in rng ((U -Veblen) | b) holds
z is_a_fixpoint_of f ) ) ;
 (U -Veblen) . a in rng ((U -Veblen) | b) by A16, A18, A17, FUNCT_1:def_3;
hence  ((U -Veblen) . b) . c is_a_fixpoint_of (U -Veblen) . a by A19; ::_thesis: verum
end;
 for b being ordinal number holds S1[b] from ORDINAL2:sch_1(A2, A3, A11);
hence  ( not c in dom ((U -Veblen) . b) or ((U -Veblen) . b) . c is_a_fixpoint_of (U -Veblen) . a ) by A1; ::_thesis: verum
end;

theorem :: ORDINAL6:59
for a being ordinal number
for l being limit_ordinal non empty Ordinal
for U being Universe st l in U & ( for c being ordinal number st c in l holds
a is_a_fixpoint_of (U -Veblen) . c ) holds
a is_a_fixpoint_of lims ((U -Veblen) | l)
proof
let a be ordinal number ; ::_thesis: for l being limit_ordinal non empty Ordinal
for U being Universe st l in U & ( for c being ordinal number st c in l holds
a is_a_fixpoint_of (U -Veblen) . c ) holds
a is_a_fixpoint_of lims ((U -Veblen) | l)
let l be limit_ordinal non empty Ordinal; ::_thesis: for U being Universe st l in U & ( for c being ordinal number st c in l holds
a is_a_fixpoint_of (U -Veblen) . c ) holds
a is_a_fixpoint_of lims ((U -Veblen) | l)
let U be Universe; ::_thesis: ( l in U & ( for c being ordinal number st c in l holds
a is_a_fixpoint_of (U -Veblen) . c ) implies a is_a_fixpoint_of lims ((U -Veblen) | l) )
assume A1: l in U ; ::_thesis: ( ex c being ordinal number st
( c in l & not a is_a_fixpoint_of (U -Veblen) . c ) or a is_a_fixpoint_of lims ((U -Veblen) | l) )
assume A2: for c being ordinal number st c in l holds
a is_a_fixpoint_of (U -Veblen) . c ; ::_thesis: a is_a_fixpoint_of lims ((U -Veblen) | l)
set F = U -Veblen ;
set g = (U -Veblen) | l;
set X =  {  ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l)  }  ;
set u = union  {  ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l)  }  ;
A3: 0 in l by ORDINAL3:8;
then  omega c= l by ORDINAL1:def_11;
then reconsider o = omega as non trivial Ordinal of U by A1, CLASSES1:def_1;
 (U -Veblen) . 0 = U exp o by Def15;
then reconsider f0 = (U -Veblen) . 0 as normal Ordinal-Sequence of U ;
A4: f0 = ((U -Veblen) | l) . 0 by FUNCT_1:49, ORDINAL3:8;
then A5: ( dom (lims ((U -Veblen) | l)) = dom f0 & dom f0 = On U ) by Def12, FUNCT_2:def_1;
A6: a is_a_fixpoint_of f0 by A2, ORDINAL3:8;
then A7: ( a in On U & a = f0 . a ) by A5, ABIAN:def_3;
A8: dom (U -Veblen) = On U by Def15;
 l in On U by A1, ORDINAL1:def_9;
then  l c= dom (U -Veblen) by A8, ORDINAL1:def_2;
then A9: dom ((U -Veblen) | l) = l by RELAT_1:62;
set lg = lims ((U -Veblen) | l);
thus  a in dom (lims ((U -Veblen) | l)) by A5, A6, ABIAN:def_3; :: according to ABIAN:def_3 ::_thesis: a = (lims ((U -Veblen) | l)) . a
A10: (lims ((U -Veblen) | l)) . a = union  {  ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l)  }  by A5, A7, Def12;
 {a} =  {  ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l)  }
proof
 a in  {  ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l)  }  by A3, A9, A7, A4;
hence  {a} c=  {  ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l)  }  by ZFMISC_1:31; :: according to XBOOLE_0:def_10 ::_thesis:  {  ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l)  }  c= {a}
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l)  }  or x in {a} )
assume  x in  {  ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l)  }  ; ::_thesis: x in {a}
then consider d being Element of dom ((U -Veblen) | l) such that
A11: ( x = (((U -Veblen) | l) . d) . a & d in dom ((U -Veblen) | l) ) ;
 ((U -Veblen) | l) . d = (U -Veblen) . d by A11, FUNCT_1:47;
then  a is_a_fixpoint_of ((U -Veblen) | l) . d by A2, A9;
then  x = a by A11, ABIAN:def_3;
hence  x in {a} by TARSKI:def_1; ::_thesis: verum
end;
hence  a = (lims ((U -Veblen) | l)) . a by A10, ZFMISC_1:25; ::_thesis: verum
end;

theorem Th60: :: ORDINAL6:60
for a, b, c being ordinal number
for U being Universe st a c= b & b in U & omega in U & c in dom ((U -Veblen) . b) & ( for c being ordinal number st c in b holds
(U -Veblen) . c is normal ) holds
((U -Veblen) . a) . c c= ((U -Veblen) . b) . c
proof
let a, b, c be ordinal number ; ::_thesis: for U being Universe st a c= b & b in U & omega in U & c in dom ((U -Veblen) . b) & ( for c being ordinal number st c in b holds
(U -Veblen) . c is normal ) holds
((U -Veblen) . a) . c c= ((U -Veblen) . b) . c
let U be Universe; ::_thesis: ( a c= b & b in U & omega in U & c in dom ((U -Veblen) . b) & ( for c being ordinal number st c in b holds
(U -Veblen) . c is normal ) implies ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c )
assume A1: ( a c= b & b in U & omega in U & c in dom ((U -Veblen) . b) ) ; ::_thesis: ( ex c being ordinal number st
( c in b & not (U -Veblen) . c is normal ) or ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c )
set F = U -Veblen ;
defpred S1[ Ordinal] means  for a, c being ordinal number st a c= $1 & $1 in U & c in dom ((U -Veblen) . $1) & ( for c being ordinal number st c in $1 holds
(U -Veblen) . c is normal ) holds
((U -Veblen) . a) . c c= ((U -Veblen) . $1) . c;
A2: S1[ 0 ] ;
A3: for b being ordinal number st S1[b] holds
S1[ succ b]
proof
let b be ordinal number ; ::_thesis: ( S1[b] implies S1[ succ b] )
assume A4: S1[b] ; ::_thesis: S1[ succ b]
let a, c be ordinal number ; ::_thesis: ( a c= succ b & succ b in U & c in dom ((U -Veblen) . (succ b)) & ( for c being ordinal number st c in succ b holds
(U -Veblen) . c is normal ) implies ((U -Veblen) . a) . c c= ((U -Veblen) . (succ b)) . c )
assume that
A5: a c= succ b and
A6: succ b in U and
A7: c in dom ((U -Veblen) . (succ b)) ; ::_thesis: ( ex c being ordinal number st
( c in succ b & not (U -Veblen) . c is normal ) or ((U -Veblen) . a) . c c= ((U -Veblen) . (succ b)) . c )
assume A8: for c being ordinal number st c in succ b holds
(U -Veblen) . c is normal ; ::_thesis: ((U -Veblen) . a) . c c= ((U -Veblen) . (succ b)) . c
 succ b in On U by A6, ORDINAL1:def_9;
then A9: (U -Veblen) . (succ b) = criticals ((U -Veblen) . b) by Def15;
then A10: dom ((U -Veblen) . (succ b)) c= dom ((U -Veblen) . b) by Th32;
A11: b in succ b by ORDINAL1:6;
then A12: b in U by A6, ORDINAL1:10;
 (U -Veblen) . b is normal by A8, ORDINAL1:6;
then A13: ((U -Veblen) . b) . c c= ((U -Veblen) . (succ b)) . c by A7, A9, Th45;
A14: for c being ordinal number st c in b holds
(U -Veblen) . c is normal by A8, A11, ORDINAL1:10;
percases ( a = succ b or a c= b ) by A5, ORDINAL5:1;
suppose a = succ b ; ::_thesis: ((U -Veblen) . a) . c c= ((U -Veblen) . (succ b)) . c
hence  ((U -Veblen) . a) . c c= ((U -Veblen) . (succ b)) . c ; ::_thesis: verum
end;
suppose a c= b ; ::_thesis: ((U -Veblen) . a) . c c= ((U -Veblen) . (succ b)) . c
then  ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c by A4, A7, A10, A12, A14;
hence  ((U -Veblen) . a) . c c= ((U -Veblen) . (succ b)) . c by A13, XBOOLE_1:1; ::_thesis: verum
end;
end;
end;
A15: for b being ordinal number st b <> {} & b is limit_ordinal & ( for d being ordinal number st d in b holds
S1[d] ) holds
S1[b]
proof
let b be ordinal number ; ::_thesis: ( b <> {} & b is limit_ordinal & ( for d being ordinal number st d in b holds
S1[d] ) implies S1[b] )
assume A16: ( b <> {} & b is limit_ordinal ) ; ::_thesis: ( ex d being ordinal number st
( d in b & not S1[d] ) or S1[b] )
assume  for d being ordinal number st d in b holds
S1[d] ; ::_thesis: S1[b]
let a, c be ordinal number ; ::_thesis: ( a c= b & b in U & c in dom ((U -Veblen) . b) & ( for c being ordinal number st c in b holds
(U -Veblen) . c is normal ) implies ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c )
assume A17: a c= b ; ::_thesis: ( not b in U or not c in dom ((U -Veblen) . b) or ex c being ordinal number st
( c in b & not (U -Veblen) . c is normal ) or ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c )
percases ( a = b or a c< b ) by A17, XBOOLE_0:def_8;
suppose a = b ; ::_thesis: ( not b in U or not c in dom ((U -Veblen) . b) or ex c being ordinal number st
( c in b & not (U -Veblen) . c is normal ) or ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c )
hence  ( not b in U or not c in dom ((U -Veblen) . b) or ex c being ordinal number st
( c in b & not (U -Veblen) . c is normal ) or ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c ) ; ::_thesis: verum
end;
supposeA18: a c< b ; ::_thesis: ( not b in U or not c in dom ((U -Veblen) . b) or ex c being ordinal number st
( c in b & not (U -Veblen) . c is normal ) or ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c )
then A19: a in b by ORDINAL1:11;
assume  b in U ; ::_thesis: ( not c in dom ((U -Veblen) . b) or ex c being ordinal number st
( c in b & not (U -Veblen) . c is normal ) or ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c )
then A20: b in On U by ORDINAL1:def_9;
then A21: (U -Veblen) . b = criticals ((U -Veblen) | b) by A16, Def15;
 dom (U -Veblen) = On U by Def15;
then  b c= dom (U -Veblen) by A20, ORDINAL1:def_2;
then A22: dom ((U -Veblen) | b) = b by RELAT_1:62;
assume A23: c in dom ((U -Veblen) . b) ; ::_thesis: ( ex c being ordinal number st
( c in b & not (U -Veblen) . c is normal ) or ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c )
assume A24: for c being ordinal number st c in b holds
(U -Veblen) . c is normal ; ::_thesis: ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c
A25: now__::_thesis:_for_c_being_ordinal_number_st_c_in_dom_((U_-Veblen)_|_b)_holds_
((U_-Veblen)_|_b)_._c_is_normal
let c be ordinal number ; ::_thesis: ( c in dom ((U -Veblen) | b) implies ((U -Veblen) | b) . c is normal )
assume  c in dom ((U -Veblen) | b) ; ::_thesis: ((U -Veblen) | b) . c is normal
then  ( c in b & ((U -Veblen) | b) . c = (U -Veblen) . c ) by A22, FUNCT_1:49;
hence  ((U -Veblen) | b) . c is normal by A24; ::_thesis: verum
end;
A26: ((U -Veblen) | b) . a in rng ((U -Veblen) | b) by A19, A22, FUNCT_1:def_3;
 ((U -Veblen) | b) . a = (U -Veblen) . a by A18, FUNCT_1:49, ORDINAL1:11;
hence  ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c by A19, A21, A22, A23, A25, A26, Th54; ::_thesis: verum
end;
end;
end;
 for b being ordinal number holds S1[b] from ORDINAL2:sch_1(A2, A3, A15);
hence  ( ex c being ordinal number st
( c in b & not (U -Veblen) . c is normal ) or ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c ) by A1; ::_thesis: verum
end;

theorem Th61: :: ORDINAL6:61
for a, b being ordinal number
for l being limit_ordinal non empty Ordinal
for U being Universe st l in U & a in U & b in l & ( for c being ordinal number st c in l holds
(U -Veblen) . c is normal Ordinal-Sequence of U ) holds
(lims ((U -Veblen) | l)) . a is_a_fixpoint_of (U -Veblen) . b
proof
let a, b be ordinal number ; ::_thesis: for l being limit_ordinal non empty Ordinal
for U being Universe st l in U & a in U & b in l & ( for c being ordinal number st c in l holds
(U -Veblen) . c is normal Ordinal-Sequence of U ) holds
(lims ((U -Veblen) | l)) . a is_a_fixpoint_of (U -Veblen) . b
let l be limit_ordinal non empty Ordinal; ::_thesis: for U being Universe st l in U & a in U & b in l & ( for c being ordinal number st c in l holds
(U -Veblen) . c is normal Ordinal-Sequence of U ) holds
(lims ((U -Veblen) | l)) . a is_a_fixpoint_of (U -Veblen) . b
let U be Universe; ::_thesis: ( l in U & a in U & b in l & ( for c being ordinal number st c in l holds
(U -Veblen) . c is normal Ordinal-Sequence of U ) implies (lims ((U -Veblen) | l)) . a is_a_fixpoint_of (U -Veblen) . b )
assume that
A1: l in U and
A2: a in U and
A3: b in l and
A4: for c being ordinal number st c in l holds
(U -Veblen) . c is normal Ordinal-Sequence of U ; ::_thesis: (lims ((U -Veblen) | l)) . a is_a_fixpoint_of (U -Veblen) . b
set F = U -Veblen ;
set g = (U -Veblen) | l;
set X =  {  ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l)  }  ;
set u = union  {  ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l)  }  ;
A5: 0 in l by ORDINAL3:8;
reconsider f0 = (U -Veblen) . 0, f = (U -Veblen) . b as normal Ordinal-Sequence of U by A3, A4, ORDINAL3:8;
A6: ( f0 = ((U -Veblen) | l) . 0 & f = ((U -Veblen) | l) . b ) by A3, FUNCT_1:49, ORDINAL3:8;
then A7: dom (lims ((U -Veblen) | l)) = dom f0 by Def12
.= On U by FUNCT_2:def_1 ;
A8: dom (U -Veblen) = On U by Def15;
 l in On U by A1, ORDINAL1:def_9;
then  l c= dom (U -Veblen) by A8, ORDINAL1:def_2;
then A9: dom ((U -Veblen) | l) = l by RELAT_1:62;
then A10: (((U -Veblen) | l) . b) . a in  {  ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l)  }  by A3;
now__::_thesis:_for_c_being_ordinal_number_st_c_in_dom_((U_-Veblen)_|_l)_holds_
((U_-Veblen)_|_l)_._c_is_Ordinal-Sequence_of_U
let c be ordinal number ; ::_thesis: ( c in dom ((U -Veblen) | l) implies ((U -Veblen) | l) . c is Ordinal-Sequence of U )
assume A11: c in dom ((U -Veblen) | l) ; ::_thesis: ((U -Veblen) | l) . c is Ordinal-Sequence of U
then  ((U -Veblen) | l) . c = (U -Veblen) . c by FUNCT_1:47;
hence  ((U -Veblen) | l) . c is Ordinal-Sequence of U by A9, A11, A4; ::_thesis: verum
end;
then reconsider lg = lims ((U -Veblen) | l) as Ordinal-Sequence of U by A1, A9, Th56;
A12: a in On U by A2, ORDINAL1:def_9;
then A13: lg . a = union  {  ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l)  }  by A7, Def12;
A14: ( dom f = On U & dom f0 = On U ) by FUNCT_2:def_1;
A15: for x being set st x in  {  ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l)  }  holds
ex y being set st
( x c= y & y in  {  ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l)  }  & y is_a_fixpoint_of f )
proof
let x be set ; ::_thesis: ( x in  {  ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l)  }  implies ex y being set st
( x c= y & y in  {  ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l)  }  & y is_a_fixpoint_of f ) )
assume A16: x in  {  ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l)  }  ; ::_thesis: ex y being set st
( x c= y & y in  {  ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l)  }  & y is_a_fixpoint_of f )
then consider d being Element of dom ((U -Veblen) | l) such that
A17: ( x = (((U -Veblen) | l) . d) . a & d in dom ((U -Veblen) | l) ) ;
reconsider f2 = (U -Veblen) . d as normal Ordinal-Sequence of U by A4, A9;
A18: f2 = ((U -Veblen) | l) . d by A9, FUNCT_1:49;
A19: dom f2 = On U by FUNCT_2:def_1;
 omega c= l by A5, ORDINAL1:def_11;
then A20: ( d in U & omega in U ) by A9, A1, CLASSES1:def_1, ORDINAL1:10;
A21: b in U by A1, A3, ORDINAL1:10;
A22: for c being ordinal number st c in b holds
(U -Veblen) . c is normal by A4, A3, ORDINAL1:10;
percases ( d c= b or b in d ) by ORDINAL1:16;
suppose d c= b ; ::_thesis: ex y being set st
( x c= y & y in  {  ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l)  }  & y is_a_fixpoint_of f )
then A23: x c= (((U -Veblen) | l) . b) . a by A12, A6, A14, A17, A18, A20, A21, A22, Th60;
take y = (((U -Veblen) | l) . (succ b)) . a; ::_thesis: ( x c= y & y in  {  ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l)  }  & y is_a_fixpoint_of f )
A24: ( b in succ b & succ b in l ) by A3, ORDINAL1:6, ORDINAL1:28;
then reconsider f1 = (U -Veblen) . (succ b) as normal Ordinal-Sequence of U by A4;
A25: f1 = ((U -Veblen) | l) . (succ b) by A24, FUNCT_1:49;
 succ b in U by A24, A1, ORDINAL1:10;
then  succ b in On U by ORDINAL1:def_9;
then A26: ( f1 = criticals f & dom f1 = On U ) by Def15, FUNCT_2:def_1;
then  f . a c= y by A12, A25, Th45;
hence  x c= y by A23, A6, XBOOLE_1:1; ::_thesis: ( y in  {  ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l)  }  & y is_a_fixpoint_of f )
thus  y in  {  ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l)  }  by A9, A24; ::_thesis: y is_a_fixpoint_of f
thus  y is_a_fixpoint_of f by A12, A25, A26, Th29; ::_thesis: verum
end;
supposeA27: b in d ; ::_thesis: ex y being set st
( x c= y & y in  {  ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l)  }  & y is_a_fixpoint_of f )
take y = x; ::_thesis: ( x c= y & y in  {  ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l)  }  & y is_a_fixpoint_of f )
thus  ( x c= y & y in  {  ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l)  }  ) by A16; ::_thesis: y is_a_fixpoint_of f
thus  y is_a_fixpoint_of f by A12, A17, A27, A18, A19, A20, Th58; ::_thesis: verum
end;
end;
end;
thus  (lims ((U -Veblen) | l)) . a in dom ((U -Veblen) . b) by A13, A14, ORDINAL1:def_9; :: according to ABIAN:def_3 ::_thesis: (lims ((U -Veblen) | l)) . a = ((U -Veblen) . b) . ((lims ((U -Veblen) | l)) . a)
hence  (lims ((U -Veblen) | l)) . a = ((U -Veblen) . b) . ((lims ((U -Veblen) | l)) . a) by A13, A10, A15, Th36; ::_thesis: verum
end;

Lm2:  for U being Universe st omega in U holds
(U -Veblen) . 0 is normal Ordinal-Sequence of U
proof
let U be Universe; ::_thesis: ( omega in U implies (U -Veblen) . 0 is normal Ordinal-Sequence of U )
assume  omega in U ; ::_thesis: (U -Veblen) . 0 is normal Ordinal-Sequence of U
then reconsider o = omega as non trivial Ordinal of U ;
 (U -Veblen) . 0 = U exp o by Def15;
hence  (U -Veblen) . 0 is normal Ordinal-Sequence of U ; ::_thesis: verum
end;

Lm3:  for a being ordinal number
for U being Universe st omega in U & a in U & (U -Veblen) . a is normal Ordinal-Sequence of U holds
(U -Veblen) . (succ a) is normal Ordinal-Sequence of U
proof
let a be ordinal number ; ::_thesis: for U being Universe st omega in U & a in U & (U -Veblen) . a is normal Ordinal-Sequence of U holds
(U -Veblen) . (succ a) is normal Ordinal-Sequence of U
let U be Universe; ::_thesis: ( omega in U & a in U & (U -Veblen) . a is normal Ordinal-Sequence of U implies (U -Veblen) . (succ a) is normal Ordinal-Sequence of U )
assume that
A1: omega in U and
A2: a in U ; ::_thesis: ( not (U -Veblen) . a is normal Ordinal-Sequence of U or (U -Veblen) . (succ a) is normal Ordinal-Sequence of U )
assume  (U -Veblen) . a is normal Ordinal-Sequence of U ; ::_thesis: (U -Veblen) . (succ a) is normal Ordinal-Sequence of U
then reconsider f = (U -Veblen) . a as normal Ordinal-Sequence of U ;
 succ a in U by A2, CLASSES2:5;
then  succ a in On U by ORDINAL1:def_9;
then  (U -Veblen) . (succ a) = criticals f by Def15;
hence  (U -Veblen) . (succ a) is normal Ordinal-Sequence of U by A1, Th44; ::_thesis: verum
end;

Lm4:  for l being limit_ordinal non empty Ordinal
for U being Universe st l in U & ( for a being ordinal number st a in l holds
(U -Veblen) . a is normal Ordinal-Sequence of U ) holds
(U -Veblen) . l is normal Ordinal-Sequence of U
proof
let l be limit_ordinal non empty Ordinal; ::_thesis: for U being Universe st l in U & ( for a being ordinal number st a in l holds
(U -Veblen) . a is normal Ordinal-Sequence of U ) holds
(U -Veblen) . l is normal Ordinal-Sequence of U
let U be Universe; ::_thesis: ( l in U & ( for a being ordinal number st a in l holds
(U -Veblen) . a is normal Ordinal-Sequence of U ) implies (U -Veblen) . l is normal Ordinal-Sequence of U )
assume A1: l in U ; ::_thesis: ( ex a being ordinal number st
( a in l & (U -Veblen) . a is not normal Ordinal-Sequence of U ) or (U -Veblen) . l is normal Ordinal-Sequence of U )
assume A2: for a being ordinal number st a in l holds
(U -Veblen) . a is normal Ordinal-Sequence of U ; ::_thesis: (U -Veblen) . l is normal Ordinal-Sequence of U
A3: l in On U by A1, ORDINAL1:def_9;
then A4: (U -Veblen) . l = criticals ((U -Veblen) | l) by Def15;
A5: dom (U -Veblen) = On U by Def15;
 l c= On U by A3, ORDINAL1:def_2;
then A6: dom ((U -Veblen) | l) = l by A5, RELAT_1:62;
A7: dom ((U -Veblen) . l) = On U
proof
set F = U -Veblen ;
set G = (U -Veblen) . l;
A8: 0 in l by ORDINAL3:8;
reconsider f0 = (U -Veblen) . 0 as normal Ordinal-Sequence of U by A2, ORDINAL3:8;
A9: dom f0 = On U by FUNCT_2:def_1;
A10: f0 = ((U -Veblen) | l) . 0 by FUNCT_1:49, ORDINAL3:8;
then  f0 in rng ((U -Veblen) | l) by A6, A8, FUNCT_1:def_3;
hence  dom ((U -Veblen) . l) c= On U by A4, A9, Th49; :: according to XBOOLE_0:def_10 ::_thesis: On U c= dom ((U -Veblen) . l)
now__::_thesis:_for_c_being_ordinal_number_st_c_in_dom_((U_-Veblen)_|_l)_holds_
((U_-Veblen)_|_l)_._c_is_Ordinal-Sequence_of_U
let c be ordinal number ; ::_thesis: ( c in dom ((U -Veblen) | l) implies ((U -Veblen) | l) . c is Ordinal-Sequence of U )
assume A11: c in dom ((U -Veblen) | l) ; ::_thesis: ((U -Veblen) | l) . c is Ordinal-Sequence of U
then  ((U -Veblen) | l) . c = (U -Veblen) . c by FUNCT_1:47;
hence  ((U -Veblen) | l) . c is Ordinal-Sequence of U by A6, A11, A2; ::_thesis: verum
end;
then reconsider lg = lims ((U -Veblen) | l) as Ordinal-Sequence of U by A1, A6, Th56;
A12: dom lg = On U by FUNCT_2:def_1;
 rng lg c= rng ((U -Veblen) . l)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng lg or y in rng ((U -Veblen) . l) )
assume  y in rng lg ; ::_thesis: y in rng ((U -Veblen) . l)
then consider x being set  such that
A13: ( x in dom lg & y = lg . x ) by FUNCT_1:def_3;
reconsider x = x as Ordinal by A13;
A14: ( x in U & y in On U ) by A12, A13, ORDINAL1:def_9;
set Y =  {  a where a is Element of dom (((U -Veblen) | l) . 0) : ( a in dom (((U -Veblen) | l) . 0) & ( for f being Ordinal-Sequence st f in rng ((U -Veblen) | l) holds
a is_a_fixpoint_of f ) )  }  ;
A15:  {  a where a is Element of dom (((U -Veblen) | l) . 0) : ( a in dom (((U -Veblen) | l) . 0) & ( for f being Ordinal-Sequence st f in rng ((U -Veblen) | l) holds
a is_a_fixpoint_of f ) )  }  is ordinal-membered by Th46;
now__::_thesis:_for_f_being_Ordinal-Sequence_st_f_in_rng_((U_-Veblen)_|_l)_holds_
y_is_a_fixpoint_of_f
let f be Ordinal-Sequence; ::_thesis: ( f in rng ((U -Veblen) | l) implies y is_a_fixpoint_of f )
assume  f in rng ((U -Veblen) | l) ; ::_thesis: y is_a_fixpoint_of f
then consider z being set  such that
A16: ( z in l & f = ((U -Veblen) | l) . z ) by A6, FUNCT_1:def_3;
 f = (U -Veblen) . z by A16, FUNCT_1:49;
hence  y is_a_fixpoint_of f by A1, A2, A16, A13, A14, Th61; ::_thesis: verum
end;
then  y in  {  a where a is Element of dom (((U -Veblen) | l) . 0) : ( a in dom (((U -Veblen) | l) . 0) & ( for f being Ordinal-Sequence st f in rng ((U -Veblen) | l) holds
a is_a_fixpoint_of f ) )  }  by A9, A10, A14;
hence  y in rng ((U -Veblen) . l) by A4, A15, Th19; ::_thesis: verum
end;
then A17: Union lg c= Union ((U -Veblen) . l) by ZFMISC_1:77;
 On U c= Union lg
proof
let a be ordinal number ; :: according to ORDINAL1:def_5 ::_thesis: ( not a in On U or a in Union lg )
assume A18: a in On U ; ::_thesis: a in Union lg
A19: a in succ a by ORDINAL1:6;
set X =  {  ((((U -Veblen) | l) . b) . (succ a)) where b is Element of dom ((U -Veblen) | l) : b in dom ((U -Veblen) | l)  }  ;
 On U is limit_ordinal by CLASSES2:51;
then A20: succ a in On U by A18, ORDINAL1:28;
then A21: lg . (succ a) = union  {  ((((U -Veblen) | l) . b) . (succ a)) where b is Element of dom ((U -Veblen) | l) : b in dom ((U -Veblen) | l)  }  by A12, Def12;
A22: f0 . (succ a) in  {  ((((U -Veblen) | l) . b) . (succ a)) where b is Element of dom ((U -Veblen) | l) : b in dom ((U -Veblen) | l)  }  by A10, A6, A8;
A23: f0 . a in f0 . (succ a) by A19, A20, A9, ORDINAL2:def_12;
 a c= f0 . a by A9, A18, ORDINAL4:10;
then  a in f0 . (succ a) by A23, ORDINAL1:12;
then  a in lg . (succ a) by A21, A22, TARSKI:def_4;
hence  a in Union lg by A12, A20, CARD_5:2; ::_thesis: verum
end;
then A24: On U c= Union ((U -Veblen) . l) by A17, XBOOLE_1:1;
A25: rng ((U -Veblen) . l) c= U
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng ((U -Veblen) . l) or x in U )
assume  x in rng ((U -Veblen) . l) ; ::_thesis: x in U
then consider y being set  such that
A26: ( y in dom ((U -Veblen) . l) & x = ((U -Veblen) . l) . y ) by FUNCT_1:def_3;
 x is_a_fixpoint_of f0 by A4, A6, A8, A10, A26, Th47;
then  ( x in dom f0 & x = f0 . x ) by ABIAN:def_3;
hence  x in U ; ::_thesis: verum
end;
assume  On U c/= dom ((U -Veblen) . l) ; ::_thesis: contradiction
then  dom ((U -Veblen) . l) in On U by ORDINAL1:16;
then reconsider d = dom ((U -Veblen) . l) as Ordinal of U by ORDINAL1:def_9;
A27: card d in card U by CLASSES2:1;
 card (rng ((U -Veblen) . l)) c= card d by CARD_1:12;
then  card (rng ((U -Veblen) . l)) in card U by A27, ORDINAL1:12;
then reconsider r = rng ((U -Veblen) . l) as Element of U by A25, CLASSES1:1;
 union r in U ;
then  Union ((U -Veblen) . l) in On U by ORDINAL1:def_9;
then  Union ((U -Veblen) . l) in Union ((U -Veblen) . l) by A24;
hence  contradiction ; ::_thesis: verum
end;
A28: rng ((U -Veblen) . l) c= On U
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng ((U -Veblen) . l) or x in On U )
assume  x in rng ((U -Veblen) . l) ; ::_thesis: x in On U
then consider y being set  such that
A29: ( y in dom ((U -Veblen) . l) & x = ((U -Veblen) . l) . y ) by FUNCT_1:def_3;
reconsider y = y as Ordinal by A29;
A30: 0 in l by ORDINAL3:8;
then  x is_a_fixpoint_of ((U -Veblen) | l) . 0 by A4, A29, A6, Th47;
then  x in dom (((U -Veblen) | l) . 0) by ABIAN:def_3;
then  ( x in dom ((U -Veblen) . 0) & (U -Veblen) . 0 is Ordinal-Sequence of U ) by A2, A30, FUNCT_1:49;
hence  x in On U by FUNCT_2:def_1; ::_thesis: verum
end;
now__::_thesis:_for_a_being_ordinal_number_st_a_in_l_holds_
((U_-Veblen)_|_l)_._a_is_normal
let a be ordinal number ; ::_thesis: ( a in l implies ((U -Veblen) | l) . a is normal )
assume A31: a in l ; ::_thesis: ((U -Veblen) | l) . a is normal
then  ((U -Veblen) | l) . a = (U -Veblen) . a by FUNCT_1:49;
hence  ((U -Veblen) | l) . a is normal by A2, A31; ::_thesis: verum
end;
then  (U -Veblen) . l is continuous by A4, A6, Th53;
hence  (U -Veblen) . l is normal Ordinal-Sequence of U by A4, A7, A28, FUNCT_2:2; ::_thesis: verum
end;

theorem Th62: :: ORDINAL6:62
for a being ordinal number
for U being Universe st omega in U & a in U holds
(U -Veblen) . a is normal Ordinal-Sequence of U
proof
let a be ordinal number ; ::_thesis: for U being Universe st omega in U & a in U holds
(U -Veblen) . a is normal Ordinal-Sequence of U
let U be Universe; ::_thesis: ( omega in U & a in U implies (U -Veblen) . a is normal Ordinal-Sequence of U )
assume A1: omega in U ; ::_thesis: ( not a in U or (U -Veblen) . a is normal Ordinal-Sequence of U )
defpred S1[ Ordinal] means ( $1 in U implies (U -Veblen) . $1 is normal Ordinal-Sequence of U );
A2: S1[ 0 ] by A1, Lm2;
A3: for b being ordinal number st S1[b] holds
S1[ succ b]
proof
let b be ordinal number ; ::_thesis: ( S1[b] implies S1[ succ b] )
 b in succ b by ORDINAL1:6;
then  ( succ b in U implies b in U ) by ORDINAL1:10;
hence  ( S1[b] implies S1[ succ b] ) by A1, Lm3; ::_thesis: verum
end;
A4: for b being ordinal number st b <> {} & b is limit_ordinal & ( for c being ordinal number st c in b holds
S1[c] ) holds
S1[b]
proof
let b be ordinal number ; ::_thesis: ( b <> {} & b is limit_ordinal & ( for c being ordinal number st c in b holds
S1[c] ) implies S1[b] )
assume that
A5: ( b <> {} & b is limit_ordinal ) and
A6: for c being ordinal number st c in b holds
S1[c] and
A7: b in U ; ::_thesis: (U -Veblen) . b is normal Ordinal-Sequence of U
now__::_thesis:_for_a_being_ordinal_number_st_a_in_b_holds_
(U_-Veblen)_._a_is_normal_Ordinal-Sequence_of_U
let a be ordinal number ; ::_thesis: ( a in b implies (U -Veblen) . a is normal Ordinal-Sequence of U )
assume A8: a in b ; ::_thesis: (U -Veblen) . a is normal Ordinal-Sequence of U
then  a in U by A7, ORDINAL1:10;
hence  (U -Veblen) . a is normal Ordinal-Sequence of U by A6, A8; ::_thesis: verum
end;
hence  (U -Veblen) . b is normal Ordinal-Sequence of U by A5, A7, Lm4; ::_thesis: verum
end;
 for b being ordinal number holds S1[b] from ORDINAL2:sch_1(A2, A3, A4);
hence  ( not a in U or (U -Veblen) . a is normal Ordinal-Sequence of U ) ; ::_thesis: verum
end;

theorem Th63: :: ORDINAL6:63
for a being ordinal number
for U, W being Universe st omega in U & U c= W & a in U holds
(U -Veblen) . a c= (W -Veblen) . a
proof
let a be ordinal number ; ::_thesis: for U, W being Universe st omega in U & U c= W & a in U holds
(U -Veblen) . a c= (W -Veblen) . a
let U, W be Universe; ::_thesis: ( omega in U & U c= W & a in U implies (U -Veblen) . a c= (W -Veblen) . a )
assume A1: ( omega in U & U c= W ) ; ::_thesis: ( not a in U or (U -Veblen) . a c= (W -Veblen) . a )
then A2: On U c= On W by ORDINAL2:9;
defpred S1[ ordinal number ] means ( $1 in U implies (U -Veblen) . $1 c= (W -Veblen) . $1 );
A3: ( (U -Veblen) . 0 = U exp omega & (W -Veblen) . 0 = W exp omega ) by Def15;
A4: ( dom (U exp omega) = On U & dom (W exp omega) = On W ) by FUNCT_2:def_1;
now__::_thesis:_for_x_being_set_st_x_in_On_U_holds_
(U_exp_omega)_._x_=_(W_exp_omega)_._x
let x be set ; ::_thesis: ( x in On U implies (U exp omega) . x = (W exp omega) . x )
assume  x in On U ; ::_thesis: (U exp omega) . x = (W exp omega) . x
then reconsider a = x as Ordinal of U by ORDINAL1:def_9;
 a in U ;
then reconsider b = a as Ordinal of W by A1;
 (U exp omega) . a = exp (omega,b) by A1, Def8;
hence  (U exp omega) . x = (W exp omega) . x by A1, Def8; ::_thesis: verum
end;
then A5: S1[ 0 ] by A2, A3, A4, GRFUNC_1:2;
A6: for b being ordinal number st S1[b] holds
S1[ succ b]
proof
let b be ordinal number ; ::_thesis: ( S1[b] implies S1[ succ b] )
assume A7: S1[b] ; ::_thesis: S1[ succ b]
assume A8: succ b in U ; ::_thesis: (U -Veblen) . (succ b) c= (W -Veblen) . (succ b)
A9: b in succ b by ORDINAL1:6;
 ( succ b in On U & succ b in On W ) by A1, A8, ORDINAL1:def_9;
then  ( (U -Veblen) . (succ b) = criticals ((U -Veblen) . b) & (W -Veblen) . (succ b) = criticals ((W -Veblen) . b) ) by Def15;
hence  (U -Veblen) . (succ b) c= (W -Veblen) . (succ b) by A7, A9, Th40, A8, ORDINAL1:10; ::_thesis: verum
end;
A10: for b being ordinal number st b <> {} & b is limit_ordinal & ( for c being ordinal number st c in b holds
S1[c] ) holds
S1[b]
proof
let b be ordinal number ; ::_thesis: ( b <> {} & b is limit_ordinal & ( for c being ordinal number st c in b holds
S1[c] ) implies S1[b] )
assume that
A11: ( b <> {} & b is limit_ordinal ) and
A12: for c being ordinal number st c in b holds
S1[c] and
A13: b in U ; ::_thesis: (U -Veblen) . b c= (W -Veblen) . b
set g1 = (U -Veblen) | b;
set g2 = (W -Veblen) | b;
A14: ( b in On U & b in On W ) by A1, A13, ORDINAL1:def_9;
then A15: ( (U -Veblen) . b = criticals ((U -Veblen) | b) & (W -Veblen) . b = criticals ((W -Veblen) | b) ) by A11, Def15;
 ( dom (U -Veblen) = On U & dom (W -Veblen) = On W ) by Def15;
then  ( b c= dom (U -Veblen) & b c= dom (W -Veblen) ) by A14, ORDINAL1:def_2;
then A16: ( dom ((U -Veblen) | b) = b & dom ((W -Veblen) | b) = b ) by RELAT_1:62;
now__::_thesis:_for_a_being_ordinal_number_st_a_in_dom_((U_-Veblen)_|_b)_holds_
((U_-Veblen)_|_b)_._a_c=_((W_-Veblen)_|_b)_._a
let a be ordinal number ; ::_thesis: ( a in dom ((U -Veblen) | b) implies ((U -Veblen) | b) . a c= ((W -Veblen) | b) . a )
assume A17: a in dom ((U -Veblen) | b) ; ::_thesis: ((U -Veblen) | b) . a c= ((W -Veblen) | b) . a
then A18: ( ((U -Veblen) | b) . a = (U -Veblen) . a & ((W -Veblen) | b) . a = (W -Veblen) . a ) by A16, FUNCT_1:47;
 a in U by A13, A16, A17, ORDINAL1:10;
hence  ((U -Veblen) | b) . a c= ((W -Veblen) | b) . a by A12, A16, A17, A18; ::_thesis: verum
end;
hence  (U -Veblen) . b c= (W -Veblen) . b by A11, A15, A16, Th55; ::_thesis: verum
end;
 for b being ordinal number holds S1[b] from ORDINAL2:sch_1(A5, A6, A10);
hence  ( not a in U or (U -Veblen) . a c= (W -Veblen) . a ) ; ::_thesis: verum
end;

theorem Th64: :: ORDINAL6:64
for a, b being ordinal number
for U, W being Universe st omega in U & a in U & b in U & omega in W & a in W & b in W holds
((U -Veblen) . b) . a = ((W -Veblen) . b) . a
proof
let a, b be ordinal number ; ::_thesis: for U, W being Universe st omega in U & a in U & b in U & omega in W & a in W & b in W holds
((U -Veblen) . b) . a = ((W -Veblen) . b) . a
let U, W be Universe; ::_thesis: ( omega in U & a in U & b in U & omega in W & a in W & b in W implies ((U -Veblen) . b) . a = ((W -Veblen) . b) . a )
assume A1: ( omega in U & a in U & b in U & omega in W & a in W & b in W ) ; ::_thesis: ((U -Veblen) . b) . a = ((W -Veblen) . b) . a
then A2: ( a in On U & a in On W ) by ORDINAL1:def_9;
 ( (W -Veblen) . b is Ordinal-Sequence of W & (U -Veblen) . b is Ordinal-Sequence of U ) by A1, Th62;
then A3: ( dom ((U -Veblen) . b) = On U & dom ((W -Veblen) . b) = On W ) by FUNCT_2:def_1;
 ( U c= W or W in U ) by CLASSES2:53;
then  ( U c= W or W c= U ) by ORDINAL1:def_2;
then  ( (U -Veblen) . b c= (W -Veblen) . b or (W -Veblen) . b c= (U -Veblen) . b ) by A1, Th63;
hence  ((U -Veblen) . b) . a = ((W -Veblen) . b) . a by A2, A3, GRFUNC_1:2; ::_thesis: verum
end;

theorem :: ORDINAL6:65
for l being limit_ordinal non empty Ordinal
for U being Universe st l in U & ( for a being ordinal number st a in l holds
(U -Veblen) . a is normal Ordinal-Sequence of U ) holds
lims ((U -Veblen) | l) is continuous non-decreasing Ordinal-Sequence of U
proof
let l be limit_ordinal non empty Ordinal; ::_thesis: for U being Universe st l in U & ( for a being ordinal number st a in l holds
(U -Veblen) . a is normal Ordinal-Sequence of U ) holds
lims ((U -Veblen) | l) is continuous non-decreasing Ordinal-Sequence of U
let U be Universe; ::_thesis: ( l in U & ( for a being ordinal number st a in l holds
(U -Veblen) . a is normal Ordinal-Sequence of U ) implies lims ((U -Veblen) | l) is continuous non-decreasing Ordinal-Sequence of U )
set G = U -Veblen ;
assume that
A1: l in U and
A2: for a being ordinal number st a in l holds
(U -Veblen) . a is normal Ordinal-Sequence of U ; ::_thesis: lims ((U -Veblen) | l) is continuous non-decreasing Ordinal-Sequence of U
 0 in l by ORDINAL3:8;
then  omega c= l by ORDINAL1:def_11;
then A3: ( omega in U & l in On U ) by A1, CLASSES1:def_1, ORDINAL1:def_9;
then A4: ( (U -Veblen) . l = criticals ((U -Veblen) | l) & dom (U -Veblen) = On U ) by Def15;
 l c= On U by A3, ORDINAL1:def_2;
then A5: dom ((U -Veblen) | l) = l by A4, RELAT_1:62;
set g = (U -Veblen) | l;
now__::_thesis:_for_a_being_ordinal_number_st_a_in_dom_((U_-Veblen)_|_l)_holds_
((U_-Veblen)_|_l)_._a_is_Ordinal-Sequence_of_U
let a be ordinal number ; ::_thesis: ( a in dom ((U -Veblen) | l) implies ((U -Veblen) | l) . a is Ordinal-Sequence of U )
assume A6: a in dom ((U -Veblen) | l) ; ::_thesis: ((U -Veblen) | l) . a is Ordinal-Sequence of U
then  ((U -Veblen) | l) . a = (U -Veblen) . a by A5, FUNCT_1:49;
hence  ((U -Veblen) | l) . a is Ordinal-Sequence of U by A2, A5, A6; ::_thesis: verum
end;
then reconsider f = lims ((U -Veblen) | l) as Ordinal-Sequence of U by A1, A5, Th56;
 ((U -Veblen) | l) . 0 = (U -Veblen) . 0 by FUNCT_1:49, ORDINAL3:8;
then reconsider g0 = ((U -Veblen) | l) . 0 as Ordinal-Sequence of U by A2, ORDINAL3:8;
A7: dom f = On U by FUNCT_2:def_1;
deffunc H1( set ) ->  set =  {  ((((U -Veblen) | l) . b) . $1) where b is Element of dom ((U -Veblen) | l) : b in dom ((U -Veblen) | l)  }  ;
A8: f is non-decreasing
proof
let a be ordinal number ; :: according to ORDINAL5:def_2 ::_thesis: for b1 being set holds
( not a in b1 or not b1 in dom f or f . a c= f . b1 )
let b be ordinal number ; ::_thesis: ( not a in b or not b in dom f or f . a c= f . b )
assume A9: ( a in b & b in dom f ) ; ::_thesis: f . a c= f . b
then  a in dom f by ORDINAL1:10;
then A10: ( f . a = union H1(a) & f . b = union H1(b) ) by A9, Def12;
let c be ordinal number ; :: according to ORDINAL1:def_5 ::_thesis: ( not c in f . a or c in f . b )
assume  c in f . a ; ::_thesis: c in f . b
then consider x being set  such that
A11: ( c in x & x in H1(a) ) by A10, TARSKI:def_4;
consider xa being Element of dom ((U -Veblen) | l) such that
A12: ( x = (((U -Veblen) | l) . xa) . a & xa in dom ((U -Veblen) | l) ) by A11;
 ((U -Veblen) | l) . xa = (U -Veblen) . xa by A5, FUNCT_1:49;
then reconsider h = ((U -Veblen) | l) . xa as increasing Ordinal-Sequence of U by A2, A5;
 dom h = On U by FUNCT_2:def_1;
then  h . a in h . b by A7, A9, ORDINAL2:def_12;
then  h . a c= h . b by ORDINAL1:def_2;
then  ( c in h . b & h . b in H1(b) ) by A11, A12;
hence  c in f . b by A10, TARSKI:def_4; ::_thesis: verum
end;
 f is continuous
proof
let a be ordinal number ; :: according to ORDINAL2:def_13 ::_thesis: for b1 being set holds
( not a in dom f or a = {} or not a is limit_ordinal or not b1 = f . a or b1 is_limes_of f | a )
let b be ordinal number ; ::_thesis: ( not a in dom f or a = {} or not a is limit_ordinal or not b = f . a or b is_limes_of f | a )
assume A13: ( a in dom f & a <> {} & a is limit_ordinal & b = f . a ) ; ::_thesis: b is_limes_of f | a
then A14: b = union H1(a) by Def12;
A15: a c= dom f by A13, ORDINAL1:def_2;
then A16: dom (f | a) = a by RELAT_1:62;
A17: b = Union (f | a)
proof
thus  b c= Union (f | a) :: according to XBOOLE_0:def_10 ::_thesis: Union (f | a) c= b
proof
let c be ordinal number ; :: according to ORDINAL1:def_5 ::_thesis: ( not c in b or c in Union (f | a) )
assume  c in b ; ::_thesis: c in Union (f | a)
then consider x being set  such that
A18: ( c in x & x in H1(a) ) by A14, TARSKI:def_4;
consider xa being Element of dom ((U -Veblen) | l) such that
A19: ( x = (((U -Veblen) | l) . xa) . a & xa in dom ((U -Veblen) | l) ) by A18;
 ((U -Veblen) | l) . xa = (U -Veblen) . xa by A5, FUNCT_1:49;
then reconsider h = ((U -Veblen) | l) . xa as normal Ordinal-Sequence of U by A2, A5;
A20: dom h = On U by FUNCT_2:def_1;
then A21: h . a is_limes_of h | a by A7, A13, ORDINAL2:def_13;
A22: h | a is increasing by ORDINAL4:15;
A23: dom (h | a) = a by A7, A15, A20, RELAT_1:62;
then  Union (h | a) is_limes_of h | a by A13, A22, ORDINAL5:6;
then  lim (h | a) = Union (h | a) by ORDINAL2:def_10;
then  h . a = Union (h | a) by A21, ORDINAL2:def_10;
then consider y being set  such that
A24: ( y in a & c in (h | a) . y ) by A18, A19, A23, CARD_5:2;
A25: y in On U by A7, A13, A24, ORDINAL1:10;
 (h | a) . y = h . y by A24, FUNCT_1:49;
then  (h | a) . y in H1(y) by A19;
then  c in union H1(y) by A24, TARSKI:def_4;
then  c in f . y by A7, A25, Def12;
then  c in (f | a) . y by A24, FUNCT_1:49;
hence  c in Union (f | a) by A16, A24, CARD_5:2; ::_thesis: verum
end;
let c be ordinal number ; :: according to ORDINAL1:def_5 ::_thesis: ( not c in Union (f | a) or c in b )
assume  c in Union (f | a) ; ::_thesis: c in b
then consider x being set  such that
A26: ( x in dom (f | a) & c in (f | a) . x ) by CARD_5:2;
A27: (f | a) . x = f . x by A16, A26, FUNCT_1:49;
 x in dom f by A26, RELAT_1:57;
then  f . x = union H1(x) by Def12;
then consider y being set  such that
A28: ( c in y & y in H1(x) ) by A26, A27, TARSKI:def_4;
consider z being Element of dom ((U -Veblen) | l) such that
A29: ( y = (((U -Veblen) | l) . z) . x & z in dom ((U -Veblen) | l) ) by A28;
 ((U -Veblen) | l) . z = (U -Veblen) . z by A5, FUNCT_1:49;
then reconsider h = ((U -Veblen) | l) . z as normal Ordinal-Sequence of U by A2, A5;
 dom h = On U by FUNCT_2:def_1;
then  h . x in h . a by A26, A16, A13, A7, ORDINAL2:def_12;
then  h . x c= h . a by ORDINAL1:def_2;
then  ( c in h . a & h . a in H1(a) ) by A28, A29;
hence  c in b by A14, TARSKI:def_4; ::_thesis: verum
end;
 f | a is non-decreasing by A8, Th13;
hence  b is_limes_of f | a by A13, A16, A17, ORDINAL5:6; ::_thesis: verum
end;
hence  lims ((U -Veblen) | l) is continuous non-decreasing Ordinal-Sequence of U by A8; ::_thesis: verum
end;

registration
let a be ordinal number ;
cluster Tarski-Class (a \/ omega) ->  uncountable ;
coherence
 not Tarski-Class (a \/ omega) is countable
proof
set U = Tarski-Class (a \/ omega);
 ( omega c= a \/ omega & a \/ omega in Tarski-Class (a \/ omega) ) by CLASSES1:2, XBOOLE_1:7;
then  omega in Tarski-Class (a \/ omega) by CLASSES1:def_1;
hence  not Tarski-Class (a \/ omega) is countable by Th57; ::_thesis: verum
end;
end;

definition
let a, b be ordinal number ;
funca -Veblen b ->  Ordinal equals :: ORDINAL6:def 16
(((Tarski-Class ((a \/ b) \/ omega)) -Veblen) . a) . b;
coherence
 (((Tarski-Class ((a \/ b) \/ omega)) -Veblen) . a) . b is Ordinal ;
end;

:: deftheorem  defines -Veblen ORDINAL6:def_16_:_
 for a, b being ordinal number holds a -Veblen b = (((Tarski-Class ((a \/ b) \/ omega)) -Veblen) . a) . b;

definition
let n be Nat;
let b be ordinal number ;
:: original: -Veblen
redefine funcn -Veblen b ->  Ordinal equals :: ORDINAL6:def 17
(((Tarski-Class (b \/ omega)) -Veblen) . n) . b;
coherence
 n -Veblen b is Ordinal ;
compatibility
 for b1 being Ordinal holds
( b1 = n -Veblen b iff b1 = (((Tarski-Class (b \/ omega)) -Veblen) . n) . b )
proof
 n c= omega ;
then  n \/ omega = omega by XBOOLE_1:12;
hence  for b1 being Ordinal holds
( b1 = n -Veblen b iff b1 = (((Tarski-Class (b \/ omega)) -Veblen) . n) . b ) by XBOOLE_1:4; ::_thesis: verum
end;
end;

:: deftheorem  defines -Veblen ORDINAL6:def_17_:_
 for n being Nat
for b being ordinal number holds n -Veblen b = (((Tarski-Class (b \/ omega)) -Veblen) . n) . b;

theorem Th66: :: ORDINAL6:66
for a, b, c being ordinal number holds a in Tarski-Class ((a \/ b) \/ c)
proof
let a, b, c be ordinal number ; ::_thesis: a in Tarski-Class ((a \/ b) \/ c)
set U = Tarski-Class ((a \/ b) \/ c);
 ( a c= a \/ b & a \/ b c= (a \/ b) \/ c ) by XBOOLE_1:7;
then  ( a c= (a \/ b) \/ c & (a \/ b) \/ c in Tarski-Class ((a \/ b) \/ c) ) by CLASSES1:2, XBOOLE_1:1;
hence  a in Tarski-Class ((a \/ b) \/ c) by CLASSES1:def_1; ::_thesis: verum
end;

theorem Th67: :: ORDINAL6:67
for a, b being ordinal number
for U being Universe st omega in U & a in U & b in U holds
b -Veblen a = ((U -Veblen) . b) . a
proof
let a, b be ordinal number ; ::_thesis: for U being Universe st omega in U & a in U & b in U holds
b -Veblen a = ((U -Veblen) . b) . a
let U be Universe; ::_thesis: ( omega in U & a in U & b in U implies b -Veblen a = ((U -Veblen) . b) . a )
assume A1: ( omega in U & a in U & b in U ) ; ::_thesis: b -Veblen a = ((U -Veblen) . b) . a
set W = Tarski-Class ((b \/ a) \/ omega);
 ( omega in Tarski-Class ((b \/ a) \/ omega) & a in Tarski-Class ((b \/ a) \/ omega) & b in Tarski-Class ((b \/ a) \/ omega) ) by Th57, Th66;
hence  b -Veblen a = ((U -Veblen) . b) . a by A1, Th64; ::_thesis: verum
end;

theorem Th68: :: ORDINAL6:68
for a being ordinal number holds 0 -Veblen a = exp (omega,a)
proof
let a be ordinal number ; ::_thesis: 0 -Veblen a = exp (omega,a)
set b = (0 \/ a) \/ omega;
set U = Tarski-Class ((0 \/ a) \/ omega);
 (0 \/ a) \/ omega in Tarski-Class ((0 \/ a) \/ omega) by CLASSES1:2;
then A1: (0 \/ a) \/ omega in On (Tarski-Class ((0 \/ a) \/ omega)) by ORDINAL1:def_9;
 omega in On (Tarski-Class ((0 \/ a) \/ omega)) by A1, ORDINAL1:12, XBOOLE_1:7;
then A2: omega in Tarski-Class ((0 \/ a) \/ omega) by ORDINAL1:def_9;
 a in On (Tarski-Class ((0 \/ a) \/ omega)) by A1, ORDINAL1:12, XBOOLE_1:7;
then A3: a in Tarski-Class ((0 \/ a) \/ omega) by ORDINAL1:def_9;
thus 0 -Veblen a = ((Tarski-Class ((0 \/ a) \/ omega)) exp omega) . a by Def15
.= exp (omega,a) by A3, A2, Def8 ; ::_thesis: verum
end;

theorem Th69: :: ORDINAL6:69
for b, a being ordinal number holds b -Veblen ((succ b) -Veblen a) = (succ b) -Veblen a
proof
let b, a be ordinal number ; ::_thesis: b -Veblen ((succ b) -Veblen a) = (succ b) -Veblen a
set U = Tarski-Class ((b \/ a) \/ omega);
A1: omega in Tarski-Class ((b \/ a) \/ omega) by Th57;
reconsider b1 = b as Ordinal of Tarski-Class ((b \/ a) \/ omega) by Th66;
 succ b1 in On (Tarski-Class ((b \/ a) \/ omega)) by ORDINAL1:def_9;
then A2: ((Tarski-Class ((b \/ a) \/ omega)) -Veblen) . (succ b) = criticals (((Tarski-Class ((b \/ a) \/ omega)) -Veblen) . b) by Def15;
reconsider f = ((Tarski-Class ((b \/ a) \/ omega)) -Veblen) . b1, g = ((Tarski-Class ((b \/ a) \/ omega)) -Veblen) . (succ b1) as normal Ordinal-Sequence of (Tarski-Class ((b \/ a) \/ omega)) by A1, Th62;
A3: a in Tarski-Class ((b \/ a) \/ omega) by Th66;
then A4: a in On (Tarski-Class ((b \/ a) \/ omega)) by ORDINAL1:def_9;
A5: ( dom f = On (Tarski-Class ((b \/ a) \/ omega)) & dom g = On (Tarski-Class ((b \/ a) \/ omega)) ) by FUNCT_2:def_1;
set W = Tarski-Class ((b \/ (g . a)) \/ omega);
 omega in Tarski-Class ((b \/ a) \/ omega) by Th57;
then A6: ( (succ b1) -Veblen a = g . a & b1 -Veblen (g . a) = f . (g . a) ) by A3, Th67;
then  (succ b) -Veblen a is_a_fixpoint_of ((Tarski-Class ((b \/ a) \/ omega)) -Veblen) . b by A4, A2, A5, Th29;
hence  b -Veblen ((succ b) -Veblen a) = (succ b) -Veblen a by A6, ABIAN:def_3; ::_thesis: verum
end;

theorem Th70: :: ORDINAL6:70
for b, c, a being ordinal number st b in c holds
b -Veblen (c -Veblen a) = c -Veblen a
proof
let b, c, a be ordinal number ; ::_thesis: ( b in c implies b -Veblen (c -Veblen a) = c -Veblen a )
assume A1: b in c ; ::_thesis: b -Veblen (c -Veblen a) = c -Veblen a
set U = Tarski-Class ((c \/ a) \/ omega);
A2: omega in Tarski-Class ((c \/ a) \/ omega) by Th57;
A3: ( a in Tarski-Class ((c \/ a) \/ omega) & c in Tarski-Class ((c \/ a) \/ omega) ) by Th66;
then A4: b in Tarski-Class ((c \/ a) \/ omega) by A1, ORDINAL1:10;
then reconsider f = ((Tarski-Class ((c \/ a) \/ omega)) -Veblen) . b, g = ((Tarski-Class ((c \/ a) \/ omega)) -Veblen) . c as normal Ordinal-Sequence of (Tarski-Class ((c \/ a) \/ omega)) by A2, Th66, Th62;
 dom g = On (Tarski-Class ((c \/ a) \/ omega)) by FUNCT_2:def_1;
then  a in dom g by A3, ORDINAL1:def_9;
then  g . a is_a_fixpoint_of f by A1, A2, Th66, Th58;
then  g . a = f . (g . a) by ABIAN:def_3;
hence  b -Veblen (c -Veblen a) = c -Veblen a by A2, A4, Th67; ::_thesis: verum
end;

theorem Th71: :: ORDINAL6:71
for a, b, c being ordinal number holds
( a c= b iff c -Veblen a c= c -Veblen b )
proof
let a, b, c be ordinal number ; ::_thesis: ( a c= b iff c -Veblen a c= c -Veblen b )
set U = Tarski-Class ((c \/ b) \/ omega);
set W = Tarski-Class ((c \/ a) \/ omega);
A1: for n being Nat holds
( n in omega & omega in Tarski-Class ((c \/ b) \/ omega) & omega in Tarski-Class ((c \/ a) \/ omega) ) by Th57, ORDINAL1:def_12;
A2: ( b in Tarski-Class ((c \/ b) \/ omega) & c in Tarski-Class ((c \/ b) \/ omega) ) by Th66;
A3: ( a in Tarski-Class ((c \/ a) \/ omega) & c in Tarski-Class ((c \/ a) \/ omega) ) by Th66;
reconsider f = ((Tarski-Class ((c \/ b) \/ omega)) -Veblen) . c as increasing Ordinal-Sequence of (Tarski-Class ((c \/ b) \/ omega)) by A1, Th66, Th62;
reconsider g = ((Tarski-Class ((c \/ a) \/ omega)) -Veblen) . c as increasing Ordinal-Sequence of (Tarski-Class ((c \/ a) \/ omega)) by A1, Th66, Th62;
A4: ( dom f = On (Tarski-Class ((c \/ b) \/ omega)) & dom g = On (Tarski-Class ((c \/ a) \/ omega)) ) by FUNCT_2:def_1;
A5: ( b in On (Tarski-Class ((c \/ b) \/ omega)) & a in On (Tarski-Class ((c \/ a) \/ omega)) ) by A2, A3, ORDINAL1:def_9;
hereby  ::_thesis: ( c -Veblen a c= c -Veblen b implies a c= b )
assume A6: a c= b ; ::_thesis: c -Veblen a c= c -Veblen b
then A7: a in Tarski-Class ((c \/ b) \/ omega) by A2, CLASSES1:def_1;
percases ( a = b or a c< b ) by A6, XBOOLE_0:def_8;
suppose a = b ; ::_thesis: c -Veblen a c= c -Veblen b
hence  c -Veblen a c= c -Veblen b ; ::_thesis: verum
end;
suppose a c< b ; ::_thesis: c -Veblen a c= c -Veblen b
then  a in b by ORDINAL1:11;
then  f . a in f . b by A4, A5, ORDINAL2:def_12;
then  c -Veblen a in c -Veblen b by A7, A1, A2, A3, Th64;
hence  c -Veblen a c= c -Veblen b by ORDINAL1:def_2; ::_thesis: verum
end;
end;
end;
assume A8: ( c -Veblen a c= c -Veblen b & a c/= b ) ; ::_thesis: contradiction
then A9: b in a by ORDINAL1:16;
then A10: b in Tarski-Class ((c \/ a) \/ omega) by A3, ORDINAL1:10;
 g . b in g . a by A4, A5, A9, ORDINAL2:def_12;
then  c -Veblen b in c -Veblen a by A1, A2, A3, A10, Th64;
then  c -Veblen b in c -Veblen b by A8;
hence  contradiction ; ::_thesis: verum
end;

theorem Th72: :: ORDINAL6:72
for a, b, c being ordinal number holds
( a in b iff c -Veblen a in c -Veblen b )
proof
let a, b, c be ordinal number ; ::_thesis: ( a in b iff c -Veblen a in c -Veblen b )
 ( b c= a iff c -Veblen b c= c -Veblen a ) by Th71;
hence  ( a in b iff c -Veblen a in c -Veblen b ) by Th4; ::_thesis: verum
end;

theorem :: ORDINAL6:73
for a, b, c, d being ordinal number holds
( a -Veblen b in c -Veblen d iff ( ( a = c & b in d ) or ( a in c & b in c -Veblen d ) or ( c in a & a -Veblen b in d ) ) )
proof
let a, b, c, d be ordinal number ; ::_thesis: ( a -Veblen b in c -Veblen d iff ( ( a = c & b in d ) or ( a in c & b in c -Veblen d ) or ( c in a & a -Veblen b in d ) ) )
hereby  ::_thesis: ( ( ( a = c & b in d ) or ( a in c & b in c -Veblen d ) or ( c in a & a -Veblen b in d ) ) implies a -Veblen b in c -Veblen d )
assume A1: a -Veblen b in c -Veblen d ; ::_thesis: ( ( a = c & b in d ) or ( a in c & b in c -Veblen d ) or ( c in a & a -Veblen b in d ) )
percases ( a = c or a in c or c in a ) by ORDINAL1:14;
case a = c ; ::_thesis: b in d
hence  b in d by A1, Th72; ::_thesis: verum
end;
case a in c ; ::_thesis: b in c -Veblen d
then  a -Veblen (c -Veblen d) = c -Veblen d by Th70;
hence  b in c -Veblen d by A1, Th72; ::_thesis: verum
end;
case c in a ; ::_thesis: a -Veblen b in d
then  c -Veblen (a -Veblen b) = a -Veblen b by Th70;
hence  a -Veblen b in d by A1, Th72; ::_thesis: verum
end;
end;
end;
assume A2: ( ( a = c & b in d ) or ( a in c & b in c -Veblen d ) or ( c in a & a -Veblen b in d ) ) ; ::_thesis: a -Veblen b in c -Veblen d
percases ( ( a = c & b in d ) or ( a in c & b in c -Veblen d ) or ( c in a & a -Veblen b in d ) ) by A2;
suppose ( a = c & b in d ) ; ::_thesis: a -Veblen b in c -Veblen d
hence  a -Veblen b in c -Veblen d by Th72; ::_thesis: verum
end;
supposeA3: ( a in c & b in c -Veblen d ) ; ::_thesis: a -Veblen b in c -Veblen d
then  a -Veblen (c -Veblen d) = c -Veblen d by Th70;
hence  a -Veblen b in c -Veblen d by A3, Th72; ::_thesis: verum
end;
supposeA4: ( c in a & a -Veblen b in d ) ; ::_thesis: a -Veblen b in c -Veblen d
then  c -Veblen (a -Veblen b) = a -Veblen b by Th70;
hence  a -Veblen b in c -Veblen d by A4, Th72; ::_thesis: verum
end;
end;
end;

begin

theorem Th74: :: ORDINAL6:74
for U being uncountable Universe holds (U -Veblen) . 1 = criticals (U exp omega)
proof
let U be uncountable Universe; ::_thesis: (U -Veblen) . 1 = criticals (U exp omega)
set o = succ (0-element_of U);
 succ (0-element_of U) in On U by ORDINAL1:def_9;
then  (U -Veblen) . 1 = criticals ((U -Veblen) . 0) by Def15;
hence  (U -Veblen) . 1 = criticals (U exp omega) by Def15; ::_thesis: verum
end;

theorem Th75: :: ORDINAL6:75
for a being ordinal number holds 1 -Veblen a is epsilon
proof
let a be ordinal number ; ::_thesis: 1 -Veblen a is epsilon
set U = Tarski-Class (a \/ omega);
 0 -Veblen (1 -Veblen a) = (succ 0) -Veblen a by Th69;
hence  exp (omega,(1 -Veblen a)) = 1 -Veblen a by Th68; :: according to ORDINAL5:def_5 ::_thesis: verum
end;

theorem Th76: :: ORDINAL6:76
for e being epsilon Ordinal ex a being ordinal number st e = 1 -Veblen a
proof
let e be epsilon Ordinal; ::_thesis: ex a being ordinal number st e = 1 -Veblen a
set U = Tarski-Class (e \/ omega);
A1: omega in Tarski-Class (e \/ omega) by Th57;
 ( 0-element_of (Tarski-Class (e \/ omega)) = 0 & 1-element_of (Tarski-Class (e \/ omega)) = 1 ) ;
then reconsider f = ((Tarski-Class (e \/ omega)) -Veblen) . 0, g = ((Tarski-Class (e \/ omega)) -Veblen) . 1 as normal Ordinal-Sequence of (Tarski-Class (e \/ omega)) by A1, Th62;
A2: g = criticals ((Tarski-Class (e \/ omega)) exp omega) by Th74
.= criticals f by Def15 ;
A3: f . e = 0 -Veblen e
.= exp (omega,e) by Th68
.= e by ORDINAL5:def_5 ;
A4: dom f = On (Tarski-Class (e \/ omega)) by FUNCT_2:def_1;
 ( e c= e \/ omega & e \/ omega in Tarski-Class (e \/ omega) ) by CLASSES1:2, XBOOLE_1:7;
then A5: e in Tarski-Class (e \/ omega) by CLASSES1:def_1;
then  e in On (Tarski-Class (e \/ omega)) by ORDINAL1:def_9;
then  e is_a_fixpoint_of f by A3, A4, ABIAN:def_3;
then consider a being ordinal number  such that
A6: ( a in dom (criticals f) & e = (criticals f) . a ) by Th33;
take  a ; ::_thesis: e = 1 -Veblen a
set W = Tarski-Class (a \/ omega);
A7: ( a c= a \/ omega & a \/ omega in Tarski-Class (a \/ omega) ) by CLASSES1:2, XBOOLE_1:7;
 a c= e by A6, ORDINAL4:10;
then  ( omega in Tarski-Class (a \/ omega) & a in Tarski-Class (a \/ omega) & a in Tarski-Class (e \/ omega) & 1-element_of (Tarski-Class (e \/ omega)) = 1-element_of (Tarski-Class (a \/ omega)) ) by A5, A7, Th57, CLASSES1:def_1;
hence  e = 1 -Veblen a by A1, A2, A6, Th64; ::_thesis: verum
end;

Lm5:  1 -Veblen 0 = epsilon_ 0
proof
consider b being ordinal number  such that
A1: 1 -Veblen 0 = epsilon_ b by Th75, ORDINAL5:51;
consider a being ordinal number  such that
A2: epsilon_ 0 = 1 -Veblen a by Th76;
now__::_thesis:_not_b_<>_0
assume  b <> 0 ; ::_thesis: contradiction
then  epsilon_ 0 in epsilon_ b by ORDINAL3:8, ORDINAL5:44;
hence  contradiction by A1, A2, Th72; ::_thesis: verum
end;
hence  1 -Veblen 0 = epsilon_ 0 by A1; ::_thesis: verum
end;

Lm6:  for a being ordinal number st 1 -Veblen a = epsilon_ a holds
1 -Veblen (succ a) = epsilon_ (succ a)
proof
let a be ordinal number ; ::_thesis: ( 1 -Veblen a = epsilon_ a implies 1 -Veblen (succ a) = epsilon_ (succ a) )
assume A1: 1 -Veblen a = epsilon_ a ; ::_thesis: 1 -Veblen (succ a) = epsilon_ (succ a)
consider b being ordinal number  such that
A2: 1 -Veblen (succ a) = epsilon_ b by Th75, ORDINAL5:51;
consider c being ordinal number  such that
A3: epsilon_ (succ a) = 1 -Veblen c by Th76;
A4: a in succ a by ORDINAL1:6;
 epsilon_ a in epsilon_ (succ a) by ORDINAL1:6, ORDINAL5:44;
then  a in c by A1, A3, Th72;
then  succ a c= c by ORDINAL1:21;
hence  1 -Veblen (succ a) c= epsilon_ (succ a) by A3, Th71; :: according to XBOOLE_0:def_10 ::_thesis: epsilon_ (succ a) c= 1 -Veblen (succ a)
assume  epsilon_ (succ a) c/= 1 -Veblen (succ a) ; ::_thesis: contradiction
then  epsilon_ b in epsilon_ (succ a) by A2, Th4;
then  b in succ a by Th12;
then  b c= a by ORDINAL1:22;
then  epsilon_ b c= epsilon_ a by Th11;
then  succ a c= a by A1, A2, Th71;
then  a in a by A4;
hence  contradiction ; ::_thesis: verum
end;

Lm7:  for l being limit_ordinal non empty Ordinal st ( for a being ordinal number st a in l holds
1 -Veblen a = epsilon_ a ) holds
1 -Veblen l = epsilon_ l
proof
let l be limit_ordinal non empty Ordinal; ::_thesis: ( ( for a being ordinal number st a in l holds
1 -Veblen a = epsilon_ a ) implies 1 -Veblen l = epsilon_ l )
assume A1: for a being ordinal number st a in l holds
1 -Veblen a = epsilon_ a ; ::_thesis: 1 -Veblen l = epsilon_ l
set U = Tarski-Class (l \/ omega);
 0 in l by ORDINAL3:8;
then  omega c= l by ORDINAL1:def_11;
then  l \/ omega = l by XBOOLE_1:12;
then A2: l in Tarski-Class (l \/ omega) by CLASSES1:2;
A3: omega in Tarski-Class (l \/ omega) by Th57;
 1-element_of (Tarski-Class (l \/ omega)) = 1 ;
then reconsider g = ((Tarski-Class (l \/ omega)) -Veblen) . 1 as normal Ordinal-Sequence of (Tarski-Class (l \/ omega)) by A3, Th62;
reconsider o = omega as non trivial Ordinal of Tarski-Class (l \/ omega) by Th57;
set f = (Tarski-Class (l \/ omega)) exp o;
A4: g = criticals ((Tarski-Class (l \/ omega)) exp o) by Th74;
A5: dom g = On (Tarski-Class (l \/ omega)) by FUNCT_2:def_1;
then A6: l in dom g by A2, ORDINAL1:def_9;
then A7: g . l = Union (g | l) by A4, Th39
.= union (rng (g | l)) ;
 l c= dom g by A6, ORDINAL1:def_2;
then A8: dom (g | l) = l by RELAT_1:62;
now__::_thesis:_for_x_being_set_st_x_in_rng_(g_|_l)_holds_
x_c=_epsilon__l
let x be set ; ::_thesis: ( x in rng (g | l) implies x c= epsilon_ l )
assume  x in rng (g | l) ; ::_thesis: x c= epsilon_ l
then consider y being set  such that
A9: ( y in dom (g | l) & x = (g | l) . y ) by FUNCT_1:def_3;
reconsider y = y as Ordinal by A9;
A10: x = g . y by A9, FUNCT_1:47;
 y in dom g by A6, A8, A9, ORDINAL1:10;
then  ( y in Tarski-Class (l \/ omega) & 1-element_of (Tarski-Class (l \/ omega)) in Tarski-Class (l \/ omega) ) by A5, ORDINAL1:def_9;
then  x = 1 -Veblen y by A3, A10, Th67;
then  x = epsilon_ y by A1, A8, A9;
then  x in epsilon_ l by A8, A9, Th12;
hence  x c= epsilon_ l by ORDINAL1:def_2; ::_thesis: verum
end;
hence  1 -Veblen l c= epsilon_ l by A7, ZFMISC_1:76; :: according to XBOOLE_0:def_10 ::_thesis: epsilon_ l c= 1 -Veblen l
let a be ordinal number ; :: according to ORDINAL1:def_5 ::_thesis: ( not a in epsilon_ l or a in 1 -Veblen l )
assume  a in epsilon_ l ; ::_thesis: a in 1 -Veblen l
then consider b being ordinal number  such that
A11: ( b in l & a in epsilon_ b ) by ORDINAL5:47;
 epsilon_ b = 1 -Veblen b by A1, A11;
then  epsilon_ b in 1 -Veblen l by A11, Th72;
hence  a in 1 -Veblen l by A11, ORDINAL1:10; ::_thesis: verum
end;

theorem :: ORDINAL6:77
for a being ordinal number holds 1 -Veblen a = epsilon_ a
proof
let a be ordinal number ; ::_thesis: 1 -Veblen a = epsilon_ a
set U = Tarski-Class (a \/ omega);
defpred S1[ Ordinal] means 1 -Veblen $1 = epsilon_ $1;
A1: S1[ 0 ] by Lm5;
A2: for b being ordinal number st S1[b] holds
S1[ succ b] by Lm6;
A3: for b being ordinal number st b <> {} & b is limit_ordinal & ( for c being ordinal number st c in b holds
S1[c] ) holds
S1[b] by Lm7;
 for b being ordinal number holds S1[b] from ORDINAL2:sch_1(A1, A2, A3);
hence  1 -Veblen a = epsilon_ a ; ::_thesis: verum
end;