:: Veblen Hierarchy
::  by Grzegorz Bancerek
::
:: Received October 18, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies ORDINAL6, CARD_1, RELAT_1, FUNCT_1, CLASSES2, NUMBERS, TARSKI,
      XBOOLE_0, SUBSET_1, ORDINAL1, ORDINAL2, WELLORD1, WELLORD2, ABIAN,
      CARD_3, MATROID0, ORDINAL4, NAT_1, ARYTM_3, CLASSES1, VALUED_0, AFINSQ_1,
      ORDINAL5, ZFMISC_1, FINSET_1, MESFUNC8, NAGATA_1, ORDINAL3, PRE_TOPC,
      AOFA_000;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1,
      FUNCT_2, FINSET_1, ORDINAL1, ORDINAL2, NAT_1, ORDINAL3, ABIAN, WELLORD1,
      WELLORD2, CARD_1, ORDINAL4, CARD_3, NAGATA_1, AFINSQ_1, CLASSES1,
      CLASSES2, NUMBERS, MATROID0, ORDINAL5, AOFA_000;
 constructors WELLORD1, WELLORD2, CLASSES1, ABIAN, CARD_3, AFINSQ_1, ORDINAL3,
      ORDINAL5, NAT_1, RELSET_1;
 registrations XBOOLE_0, RELAT_1, RELSET_1, FUNCT_1, FINSET_1, FUNCT_2,
      ORDINAL1, ORDINAL2, CARD_1, WELLORD2, ORDINAL3, CLASSES2, CARD_5,
      ORDINAL4, CARD_LAR, ORDINAL5, CLASSES1, AFINSQ_1, SUBSET_1;
 requirements SUBSET, BOOLE, NUMERALS;
 definitions TARSKI, XBOOLE_0, FUNCT_1, WELLORD1, ABIAN, ORDINAL1, ORDINAL2,
      ORDINAL4, CARD_3, ORDINAL5;
 theorems XBOOLE_1, ZFMISC_1, RELAT_1, FUNCT_1, ORDINAL1, ORDINAL2, ORDINAL3,
      FUNCT_3, WELLORD1, WELLORD2, ORDERS_1, CARD_2, CARD_5, FUNCT_2, ORDINAL4,
      XBOOLE_0, TARSKI, ORDINAL5, NAT_1, CLASSES1, CLASSES2, CARD_1, AFINSQ_1,
      NAT_2, GRFUNC_1, ABIAN;
 schemes NAT_1, ORDINAL1, ORDINAL2, ORDINAL4, TREES_2;

begin :: Preliminaries

reserve a,b,c,d for ordinal number;
reserve l for non empty limit_ordinal Ordinal;
reserve u for Element of l;
reserve A for non empty ordinal number;
reserve e for Element of A;
reserve X,Y,x,y,z for set;
reserve n,m for Nat;

definition
  let X be set;
  attr X is ordinal-membered means :Def1:
  ex a st X c= a;
end;

registration
  cluster ordinal -> ordinal-membered for set;
  coherence
  proof
    let X be set;
    assume X is ordinal;
    hence ex a st X c= a;
  end;
  let X;
  cluster On X -> ordinal-membered;
  coherence
  proof
    take sup X;
    thus thesis by ORDINAL2:def 3;
  end;
end;

theorem Th1:
  X is ordinal-membered iff for x st x in X holds x is ordinal
  proof
    thus X is ordinal-membered implies for x st x in X holds x is ordinal
    proof assume
      ex a st X c= a;
      hence thesis;
    end;
    assume
A1: for x st x in X holds x is ordinal;
    take a = sup X;
    let x; assume
A2: x in X; then
    x is Ordinal by A1;
    hence thesis by A2,ORDINAL2:19;
end;

registration
  cluster ordinal-membered for set;
  existence
  proof
    take 0,0;
    thus 0 c= 0;
  end;
end;

registration
  let X be ordinal-membered set;
  cluster -> ordinal for Element of X;
  coherence
  proof
    let a be Element of X;
    per cases;
    suppose X is empty;
      hence thesis;
    end;
    suppose X is non empty;
      hence thesis by Th1;
    end;
  end;
end;

theorem Th2:
  X is ordinal-membered iff On X = X
  proof
    hereby assume
A1:   X is ordinal-membered;
      thus On X = X
      proof thus On X c= X by ORDINAL2:7;
        let x;
        thus thesis by A1,ORDINAL1:def 9;
      end;
    end;
    thus thesis;
  end;

theorem
  for X being ordinal-membered set holds X c= sup X
  proof
    let X be ordinal-membered set;
    let x;
    thus thesis by ORDINAL2:19;
  end;

theorem Th4:
  a c= b iff b nin a
  proof
    a c= b & b in a implies b in b;
    hence thesis by ORDINAL1:16;
  end;

theorem
  x in a\b iff b c= x & x in a
  proof
    x in a\b iff x nin b & x in a by XBOOLE_0:def 5;
    hence thesis by Th4;
  end;

registration let a,b;
  cluster a\b -> ordinal-membered;
  coherence
  proof take a;
    thus thesis;
  end;
end;

theorem Th6:
  for f being Function st f is_isomorphism_of RelIncl X, RelIncl Y
  for x,y st x in X & y in X holds x c= y iff f.x c= f.y
  proof
    let f be Function; assume
A1: f is_isomorphism_of RelIncl X, RelIncl Y;
    let x,y such that
A2: x in X & y in X;
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 thesis by A4,WELLORD2:def 1;
  end;

theorem
  for X,Y being ordinal-membered set
  for f being Function st f is_isomorphism_of RelIncl X, RelIncl Y
  for x,y 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;
    let f be Function; assume
A1: f is_isomorphism_of RelIncl X, RelIncl Y;
    let x,y;
    assume
A2: x in X & y in X;
    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,y as Ordinal by A2;
    y c= x iff b c= a by A1,A2,Th6;
    hence thesis by Th4;
  end;

theorem Th8:
  [x,y] in RelIncl X implies x c= y
  proof assume
A1: [x,y] in RelIncl X;
    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;
  end;

theorem Th9:
  for f1,f2 being T-Sequence holds f1 c= f1^f2
  proof
    let f1,f2 be T-Sequence;
    dom(f1^f2) = (dom f1)+^dom f2 by ORDINAL4:def 1; then
A1: dom f1 c= dom(f1^f2) by ORDINAL3:24;
    for x 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;
  end;

theorem Th10:
  for f1,f2 being T-Sequence holds rng(f1^f2) = rng f1 \/ rng f2
  proof let f1,f2 be T-Sequence;
    set f = f1^f2, A1 = rng f1, A2 = rng f2;
A1:  dom(f1^f2) = (dom f1)+^(dom f2) by ORDINAL4:def 1;
    thus rng(f1^f2) c= rng f1 \/ rng f2
    proof
      let y;
      assume y in rng f;
      then consider x such that
A2:   x in dom f and
A3:   y = f.x by FUNCT_1:def 3;
      reconsider x as Ordinal by A2;
      per cases;
      suppose
A4:     x in dom f1;
        then
A5:     f1.x in rng f1 by FUNCT_1:def 3;
        y = f1.x by A3,A4,ORDINAL4:def 1;
        hence thesis by A5,XBOOLE_0:def 3;
      end;
      suppose
        not x in dom f1;
        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 thesis by XBOOLE_0:def 3;
      end;
    end;
    let x; assume
A8: x in rng f1 \/ rng f2;
A9: dom f1 c= (dom f1)+^dom f2 by ORDINAL3:24;
    per cases by A8,XBOOLE_0:def 3;
    suppose x in rng f1; then
      consider z such that
A10:   z in dom f1 & x = f1.z by FUNCT_1:def 3;
      x = f.z by A10,ORDINAL4:def 1;
      hence thesis by A1,A9,A10,FUNCT_1:def 3;
    end;
    suppose x in rng f2; then
      consider z such that
A11:   z in dom f2 & x = f2.z by FUNCT_1:def 3;
      reconsider z as Ordinal by A11;
A12:   (dom f1)+^z in dom f by A1,A11,ORDINAL3:17;
      x = f.((dom f1)+^z) by A11,ORDINAL4:def 1;
      hence thesis by A12,FUNCT_1:def 3;
    end;
  end;

theorem Th11:
  a c= b iff epsilon_a c= epsilon_b
  proof
    hereby assume
      a c= 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;
    end;
    assume
A1: epsilon_a c= epsilon_b;
    assume a c/= b; then
    epsilon_b in epsilon_a by ORDINAL1:16,ORDINAL5:44; then
    epsilon_b in epsilon_b by A1;
    hence thesis;
  end;

theorem Th12:
  a in b iff epsilon_a in epsilon_b
  proof
    b c/= a iff epsilon_b c/= epsilon_a by Th11;
    hence thesis by Th4;
  end;

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

registration
  let f be Ordinal-yielding Function;
  cluster rng f -> ordinal-membered;
  coherence
  proof
    thus ex a st rng f c= a by ORDINAL2:def 4;
  end;
end;

registration
  let a;
  cluster id a -> T-Sequence-like Ordinal-yielding;
  coherence
  proof
    dom id a = a & rng id a = a;
    hence thesis by ORDINAL1:def 7,ORDINAL2:def 4;
  end;
end;

registration
  let a;
  cluster id a -> increasing for Ordinal-Sequence;
  coherence
  proof
    let f be Ordinal-Sequence such that
A1: f = id a;
    let b,c; assume
A2: b in c & c in dom f; 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 thesis by A2;
  end;
end;

registration
  let a;
  cluster id a -> continuous for Ordinal-Sequence;
  coherence
  proof
    let f be Ordinal-Sequence such that
A1: f = id a;
    let b,c; assume
A2: b in dom f & b <> {} & b is limit_ordinal & c = 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: g = id b by A1,FUNCT_3:1;
    per cases;
    case c = {};
      hence thesis by A2,A1,A3,FUNCT_1:18;
    end;
    case c <> {};
      let B,C be Ordinal; assume
A6:   B in c & c in C;
      take D = succ B;
      thus D in dom g by A2,A3,A4,A5,A6,ORDINAL1:28;
      let E be Ordinal; assume
A7:   D c= E & E in dom g; then
      g.E = E by A3,A5,FUNCT_1:18;
      hence B in g.E & g.E in C by A3,A4,A5,A6,A7,ORDINAL1:10,21;
    end;
  end;
end;

registration
  cluster non empty increasing continuous for Ordinal-Sequence;
  existence
  proof
    set A = the non empty ordinal number;
    take id A;
    thus thesis;
  end;
end;

definition
  let f be T-Sequence;
  attr f is normal means: Def2:
  f is increasing continuous Ordinal-Sequence;
end;

definition
  let f be Ordinal-Sequence;
  redefine attr f is normal means
  f is increasing continuous;
  compatibility by Def2;
end;

registration
  cluster normal -> Ordinal-yielding for T-Sequence;
  coherence by Def2;
  cluster normal -> increasing continuous for Ordinal-Sequence;
  coherence by Def2;
  cluster increasing continuous -> normal for Ordinal-Sequence;
  coherence by Def2;
end;

registration
  cluster non empty normal for T-Sequence;
  existence
  proof
    set A = the non empty ordinal number;
    take id A;
    thus thesis;
  end;
end;

theorem Th13:
  for f being Ordinal-Sequence holds
  f is non-decreasing implies f|a is non-decreasing
  proof let f be Ordinal-Sequence;
    assume
A1: for b,c st b in c & c in dom f holds f.b c= f.c;
    let b,c; assume
A2: b in c & c in dom(f|a); 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 thesis by A1,A2,A3;
  end;

definition
  let X;
  func ord-type X -> ordinal number equals
  order_type_of RelIncl On X;
  coherence;
end;

definition
  let X be ordinal-membered set;
  redefine func ord-type X equals order_type_of RelIncl X;
  compatibility by Th2;
end;

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

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

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

theorem
  ord-type {} = 0;

theorem
  ord-type {a} = 1
  proof
    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 thesis by A1,ORDINAL3:6;
  end;

theorem
  a <> b implies ord-type {a,b} = 2
  proof
    assume a <> b; 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 thesis by A1,A2,CARD_5:36;
  end;

theorem
  ord-type a = a by ORDERS_1:88;

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

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

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

theorem
  card dom numbering X = card On X
  proof
    dom numbering X = ord-type X &
    ex a st On X c= a by Th18,Def1;
    hence thesis by CARD_5:7;
  end;

theorem Th21:
  numbering X is_isomorphism_of RelIncl ord-type X, RelIncl On X
  proof
    set R1 = RelIncl ord-type X;
    set R2 = RelIncl On X;
    R2,R1 are_isomorphic by WELLORD2:def 2; then
    R1,R2 are_isomorphic by WELLORD1:40;
    hence thesis by WELLORD1:def 9;
  end;

reserve f for Ordinal-Sequence;

theorem Th22:
  f = numbering X & x in dom f & y in dom f implies (x c= y iff f.x c= f.y)
  proof assume
A1: f = numbering X & x in dom f & y in dom f; then
    dom f = ord-type X &
    f is_isomorphism_of RelIncl ord-type X, RelIncl On X by Th18,Th21;
    hence thesis by A1,Th6;
  end;

theorem Th23:
  f = numbering X & x in dom f & y in dom f implies (x in y iff f.x in f.y)
  proof assume
A1: f = numbering X & x in dom f & y in dom f; then
    y c= x iff f.y c= f.x by Th22;
    hence thesis by A1,Th4;
  end;

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

registration
  let X,Y be ordinal-membered set;
  cluster X \/ Y -> ordinal-membered;
  coherence
  proof
    consider a such that
A1: X c= a by Def1;
    consider b such that
A2: Y c= b by Def1;
    take a \/ b;
    thus thesis by A1,A2,XBOOLE_1:13;
  end;
end;

registration
  let X be ordinal-membered set, Y be set;
  cluster X \ Y -> ordinal-membered;
  coherence
  proof
    consider a such that
A1: X c= a by Def1;
    take a;
    thus thesis by A1,XBOOLE_1:1;
  end;
end;

theorem Th24:
  for X,Y being ordinal-membered set
  st for x,y 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; assume
A1: for x,y st x in X & y in Y holds x in y;
    set f = numbering X, g = numbering Y;
    set a = ord-type X, b = ord-type Y;
    set R = RelIncl(a+^b), Q = RelIncl(X\/Y);
    set R1 = RelIncl a, Q1 = RelIncl(X);
    set R2 = RelIncl b, Q2 = RelIncl(Y);
A2:  dom(f^g) = (dom f)+^dom g by ORDINAL4:def 1;
A3: dom f = a & dom g = b by Th18;
A4: rng f = X & rng g = Y by Th19;
A5: f is_isomorphism_of RelIncl a, RelIncl On X &
    g is_isomorphism_of RelIncl b, RelIncl On Y by Th21; then
A6: f is one-to-one & g is one-to-one by WELLORD1:def 7;
    thus
A7: dom(f^g) = (dom f)+^dom g by ORDINAL4:def 1
    .= field R by A3,WELLORD2:def 1;
    thus rng(f^g) = (rng f)\/rng g by Th10
    .= field Q by A4,WELLORD2:def 1; then
A8: rng(f^g) = X\/Y by WELLORD2:def 1;
A9: On X = X & On Y = Y by Th2;
    thus f^g is one-to-one
    proof
      let x,y; assume
A10:   x in dom(f^g) & y in dom(f^g) & (f^g).x = (f^g).y; then
      reconsider a = x, b = y as Ordinal;
      per cases by A10,ORDINAL1:16;
      suppose
A11:     x in dom f & y in dom f; then
        (f^g).x = f.x & (f^g).y = f.y by ORDINAL4:def 1;
        hence thesis by A6,A10,A11,FUNCT_1:def 4;
      end;
      suppose
A12:     x in dom f & dom f c= y; then
A13:     (dom f)+^(b-^dom f) = y by ORDINAL3:def 5; then
A14:     b-^dom f in dom g by A2,A10,ORDINAL3:22; then
        (f^g).x = f.x & (f^g).y = g.(b-^dom f) by A12,A13,ORDINAL4:def 1; then
        f.x in X & f.x in Y by A4,A10,A12,A14,FUNCT_1:def 3; then
        f.x in f.x by A1;
        hence thesis;
      end;
      suppose
A15:     dom f c= x & y in dom f; then
A16:     (dom f)+^(a-^dom f) = x by ORDINAL3:def 5; then
A17:     a-^dom f in dom g by A2,A10,ORDINAL3:22; then
        (f^g).y = f.y & (f^g).x = g.(a-^dom f) by A15,A16,ORDINAL4:def 1; then
        f.y in X & f.y in Y by A4,A10,A15,A17,FUNCT_1:def 3; then
        f.y in f.y by A1;
        hence thesis;
      end;
      suppose dom f c= x & dom f c= y; then
A18:     (dom f)+^(a-^dom f) = x & (dom f)+^(b-^dom f) = y
        by ORDINAL3:def 5; then
A19:     a-^dom f in dom g & b-^dom f in dom g by A2,A10,ORDINAL3:22; then
        (f^g).y = g.(b-^dom f) & (f^g).x = g.(a-^dom f) by A18,ORDINAL4:def 1;
        hence thesis by A6,A10,A18,A19,FUNCT_1:def 4;
      end;
    end;
    let x,y;
A20: field R = a+^b by WELLORD2:def 1;
    hereby assume
A21:   [x,y] in R;
      hence
A22:   x in field R & y in field R by RELAT_1:15; then
A23:   x c= y by A21,A20,WELLORD2:def 1;
A24:   (f^g).x in X\/Y & (f^g).y in X\/Y by A7,A8,A22,FUNCT_1:def 3;
      thus [(f^g).x,(f^g).y] in Q
      proof
        reconsider x,y as Ordinal by A20,A22;
        per cases by ORDINAL1:16;
        suppose
A25:       x in dom f & y in dom f; then
A26:       [x,y] in RelIncl a by A3,A23,WELLORD2:def 1;
          (f^g).x = f.x & (f^g).y = f.y by A25,ORDINAL4:def 1; then
A27:       [(f^g).x, (f^g).y] in Q1 by A9,A5,A26,WELLORD1:def 7; then
          (f^g).x in field Q1 & (f^g).y in field Q1 by RELAT_1:15; then
          (f^g).x in X & (f^g).y in X by WELLORD2:def 1; then
          (f^g).x c= (f^g).y by A27,WELLORD2:def 1;
          hence thesis by A24,WELLORD2:def 1;
        end;
        suppose
A28:       x in dom f & dom f c= y; then
A29:       (dom f)+^(y-^dom f) = y by ORDINAL3:def 5; then
A30:       y-^dom f in dom g by A3,A20,A22,ORDINAL3:22; then
          (f^g).x = f.x & (f^g).y = g.(y-^dom f) by A28,A29,ORDINAL4:def 1;
then
          (f^g).x in X & (f^g).y in Y by A4,A28,A30,FUNCT_1:def 3; then
          (f^g).x in (f^g).y by A1; then
          (f^g).x c= (f^g).y by ORDINAL1:def 2;
          hence thesis by A24,WELLORD2:def 1;
        end;
        suppose
          dom f c= x & y in dom f; then
          y in x; then
          y in y by A23;
          hence thesis;
        end;
        suppose dom f c= x & dom f c= y; then
A31:       (dom f)+^(x-^dom f) = x & (dom f)+^(y-^dom f) = y
          by ORDINAL3:def 5; then
A32:       x-^dom f in dom g & y-^dom f in dom g by A3,A20,A22,ORDINAL3:22;
          x-^a c= y-^a by A23,ORDINAL3:59; then
A33:       [x-^a,y-^a] in RelIncl b by A32,A3,WELLORD2:def 1;
          (f^g).y = g.(y-^dom f) & (f^g).x = g.(x-^dom f)
          by A31,A32,ORDINAL4:def 1; then
A34:       [(f^g).x, (f^g).y] in Q2 by A9,A3,A5,A33,WELLORD1:def 7; then
          (f^g).x in field Q2 & (f^g).y in field Q2 by RELAT_1:15; then
          (f^g).x in Y & (f^g).y in Y by WELLORD2:def 1; then
          (f^g).x c= (f^g).y by A34,WELLORD2:def 1;
          hence thesis by A24,WELLORD2:def 1;
        end;
      end;
    end;
    assume
A35: x in field R & y in field R & [(f^g).x,(f^g).y] in Q; then
A36: (f^g).x c= (f^g).y by Th8;
A37: field R1 = a & field R2 = b by WELLORD2:def 1;
    reconsider x,y as Ordinal by A20,A35;
    per cases by ORDINAL1:16;
    suppose
A38:   x in dom f & y in dom f; then
A39:   (f^g).x = f.x & (f^g).y = f.y by ORDINAL4:def 1;
      f.x in X & f.y in X by A4,A38,FUNCT_1:def 3; then
      [f.x, f.y] in Q1 by A39,A36,WELLORD2:def 1; then
      [x,y] in R1 by A9,A38,A37,A3,A5,WELLORD1:def 7; then
      x c= y by Th8;
      hence thesis by A20,A35,WELLORD2:def 1;
    end;
    suppose
      x in dom f & dom f c= y; then
      x c= y by ORDINAL1:def 2;
      hence thesis by A20,A35,WELLORD2:def 1;
    end;
    suppose
A40:   dom f c= x & y in dom f; then
A41:   (f^g).y = f.y by ORDINAL4:def 1;
A42:   f.y in X by A4,A40,FUNCT_1:def 3;
A43:   (dom f)+^(x-^dom f) = x by A40,ORDINAL3:def 5; then
A44:   x-^dom f in dom g by A3,A20,A35,ORDINAL3:22; then
A45:   (f^g).x = g.(x-^dom f) by A43,ORDINAL4:def 1;
      g.(x-^dom f) in Y by A4,A44,FUNCT_1:def 3; then
      (f^g).y in (f^g).x by A41,A42,A45,A1; then
      (f^g).y in (f^g).y by A36;
      hence thesis;
    end;
    suppose dom f c= x & dom f c= y; then
A46:   (dom f)+^(x-^dom f) = x & (dom f)+^(y-^dom f) = y
      by ORDINAL3:def 5; then
A47:   x-^dom f in dom g & y-^dom f in dom g by A3,A20,A35,ORDINAL3:22; then
A48:   g.(y-^dom f) in Y & g.(x-^dom f) in Y by A4,FUNCT_1:def 3;
      (f^g).y = g.(y-^dom f) & (f^g).x = g.(x-^dom f)
      by A46,A47,ORDINAL4:def 1; then
      [g.(x-^dom f), g.(y-^dom f)] in Q2
      by A48,A36,WELLORD2:def 1; then
      [(x-^dom f), (y-^dom f)] in R2 by A9,A37,A3,A5,A47,WELLORD1:def 7; then
      x-^dom f c= y-^dom f by Th8; then
      x c= y by A46,ORDINAL3:18;
      hence thesis by A20,A35,WELLORD2:def 1;
    end;
  end;

theorem Th25:
  for X,Y being ordinal-membered set
  st for x,y 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; assume
A1: for x,y st x in X & y in Y holds x in y;
    set f = numbering X, g = numbering Y, h = numbering(X\/Y);
    set a = ord-type X, b = ord-type Y;
    set P = RelIncl(a+^b), 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: h is_isomorphism_of R,Q by Th21;
A4: f^g is_isomorphism_of P,Q by A1,Th24; then
A5: P,Q are_isomorphic & R,Q are_isomorphic by A3,WELLORD1:def 8; then
    Q,R are_isomorphic by WELLORD1:40; then
    a+^b = 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;
  end;

theorem
  for X,Y being ordinal-membered set
  st for x,y 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;
    assume for x,y st x in X & y in Y holds x in 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;
  end;

begin :: Fixpoints of a Normal Function

theorem Th27:
  for f being Function st x is_a_fixpoint_of f holds x in rng f
  proof
    let f be Function;
    assume x in dom f & x = f.x;
    hence thesis by FUNCT_1:def 3;
  end;

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

theorem Th28:
  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
    set X = {a where a is Element of dom f: a is_a_fixpoint_of f};
    now
      let x;
      assume x in X; then
      ex a being Element of dom f st x = a & a is_a_fixpoint_of f;
      hence x is ordinal;
    end; then
    X is ordinal-membered by Th1;
    hence thesis by Th2;
  end;

theorem Th29:
  x in dom criticals f implies (criticals f).x is_a_fixpoint_of f
  proof set a = x;
    set X = {b where b is Element of dom f: b is_a_fixpoint_of f};
    set g = criticals f;
    assume a in dom g; then
    g.a in rng g by FUNCT_1:def 3; then
    g.a in On X by Th18; then
    g.a in X by Th28; then
    ex b being Element of dom f st g.a = b & b is_a_fixpoint_of f;
    hence thesis;
  end;

theorem Th30:
  rng criticals f = {a where a is Element of dom f: a is_a_fixpoint_of f} &
  rng criticals f c= rng f
  proof
    set X = {a where a is Element of dom f: a is_a_fixpoint_of f};
    On X = X by Th28;
    hence
A1: rng criticals f = X by Th18;
    let x; assume x in rng criticals f; then
    ex a being Element of dom f st x = a & a is_a_fixpoint_of f by A1;
    hence thesis by Th27;
  end;

registration let f;
  cluster criticals f -> increasing;
  coherence;
end;

theorem
  x in dom criticals f implies x c= (criticals f).x by ORDINAL4:10;

theorem Th32:
  dom criticals f c= dom f
  proof let x be Ordinal;
    set X = {a where a is Element of dom f: a is_a_fixpoint_of f};
    assume
A1: x in dom criticals f; then
    (criticals f).x in rng criticals f by FUNCT_1:def 3; then
    (criticals f).x in On X by Th18; then
    (criticals f).x in X 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 thesis by ORDINAL1:12;
  end;

theorem Th33:
  b is_a_fixpoint_of f implies
  ex a st a in dom criticals f & b = (criticals f).a
  proof
    set X = {a where a is Element of dom f: a is_a_fixpoint_of f};
    assume
A1: b is_a_fixpoint_of f; then
    b in dom f by ABIAN:def 3; then
    b in X by A1; then
    b in rng criticals f by Th30; then
    ex x st x in dom criticals f & b = (criticals f).x by FUNCT_1:def 3;
    hence thesis;
  end;

theorem
  a in dom criticals f & b is_a_fixpoint_of f & (criticals f).a in b
  implies succ a in dom criticals f
  proof set g = criticals f;
    assume that
A1: a in dom g and
A2: b is_a_fixpoint_of f and
A3: g.a in b;
    consider c such that
A4: c in dom g & b = g.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;
  end;

theorem
  succ a in dom criticals f & b is_a_fixpoint_of f & (criticals f).a in b
  implies (criticals f).succ a c= b
  proof set g = criticals f;
    set Y = {c where c is Element of dom f: c is_a_fixpoint_of f};
    set X = ord-type Y;
    assume
A1: succ a in dom g & b is_a_fixpoint_of f & g.a in b; then
    consider c such that
A2: c in dom g & b = g.c by Th33;
    a in succ a by ORDINAL1:6; then
A3: a in dom g & g.a in g.succ a by A1,ORDINAL1:10,ORDINAL2:def 12;
    On Y = Y by Th28; then
A4: g is_isomorphism_of RelIncl X, RelIncl Y by Th21;
A5: dom g = X by Th18;
    b c/= g.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 g.succ a c= b by A2,ORDINAL4:9;
  end;

theorem Th36:
  f is normal & union X in dom f & X is non empty &
  (for x st x in X ex y st x c= y & y in X & y is_a_fixpoint_of f)
  implies union X = f.union X
  proof assume that
A1: f is normal and
A2: union X in dom f & X is non empty and
A3: for x st x in X ex y st x c= y & y in X & y is_a_fixpoint_of f;
    reconsider l = union X as Ordinal by A2;
    per cases;
    suppose
      ex a st a in X & for b st b in X holds b c= a; then
      consider a such that
A4:   a in X & for b st b in X holds b c= a;
      now
        let x; assume
        x in X; then
        consider y 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;
      end; then
      union X c= a & a c= union X by A4,ZFMISC_1:74,76; then
A6:   union X = a by XBOOLE_0:def 10; then
      consider y 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;
    end;
    suppose
A8:   not ex a st a in X & for b st b in X holds b c= a;
      set y0 = the Element of X;
      consider x0 being set such that
A9:   y0 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 such that
A11:   b in X & b c/= x0 by A9,A8;
A12:   x0 in b by A10,A11,Th4;
      now
        let a; assume a in l; then
        consider x such that
A13:     a in x & x in X by TARSKI:def 4;
        consider y 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 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;
      end; then
      reconsider l as non empty limit_ordinal Ordinal
      by A12,A11,ORDINAL1:28,TARSKI:def 4;
      thus union X c= f.union X by A2,A1,ORDINAL4:10;
      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; assume x in f.union X; then
      consider z such that
A20:   z in dom g & x in g.z by A19,CARD_5:2;
      consider y 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,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;
    end;
  end;

theorem Th37:
  f is normal & union X in dom f & X is non empty &
  (for x st x in X holds x is_a_fixpoint_of f)
  implies union X = f.union X
  proof assume that
A1: f is normal and
A2: union X in dom f & X is non empty and
A3: for x st x in X holds x is_a_fixpoint_of f;
    for x st x in X ex y st x c= y & y in X & y is_a_fixpoint_of f by A3;
    hence thesis by A1,A2,Th36;
  end;

theorem Th38:
  l c= dom criticals f & a is_a_fixpoint_of f &
  (for x st x in l holds (criticals f).x in a)
  implies l in dom criticals f
  proof set g = criticals f;
    assume that
A1: l c= dom g and
A2: a is_a_fixpoint_of f and
A3: for x st x in l holds g.x in a;
    consider b such that
A4: b in dom g & a = g.b by A2,Th33;
    l c= b
    proof
      let x be Ordinal; assume x in l; then
      x in dom g & g.x in g.b by A1,A3,A4;
      hence x in b by A4,Th23;
    end;
    hence l in dom criticals f by A4,ORDINAL1:12;
  end;

theorem Th39:
  f is normal & l in dom criticals f implies
  (criticals f).l = Union ((criticals f)|l)
  proof set g = criticals f;
    reconsider h = g|l as increasing Ordinal-Sequence by ORDINAL4:15;
    set X = rng h;
    assume
A1: f is normal & l in dom g; then
    g.l is_a_fixpoint_of f by Th29; then
A2: g.l in dom f & f.(g.l) = g.l by ABIAN:def 3;
A3: l c= dom g by A1,ORDINAL1:def 2; then
A4: dom h = l by RELAT_1:62;
A5: for x st x in X holds x is_a_fixpoint_of f
    proof
      let x; assume x in X; then
      consider y such that
A6:   y in dom h & x = h.y by FUNCT_1:def 3;
      x = g.y & y in dom g by A3,A4,A6,FUNCT_1:47;
      hence thesis by Th29;
    end;
    reconsider u = union X as Ordinal;
A7: h <> {} by A4;
    now
      let x; assume x in X; then
      consider y such that
A8:   y in dom h & x = h.y by FUNCT_1:def 3;
      x = g.y & y in dom g by A3,A4,A8,FUNCT_1:47; then
      x in g.l by A1,A4,A8,ORDINAL2:def 12;
      hence x c= g.l by ORDINAL1:def 2;
    end; then
A9: union X c= g.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 such that
A11: a in dom g & u = g.a by Th33;
    a = l
    proof
      thus a c= l by A1,A11,A9,Th22;
      let x be Ordinal; assume
A12:   x in l; then
A13:   succ x in l by ORDINAL1:28; then
A14:   g.x = h.x & g.succ x = h.succ x & h.succ x in X
      by A4,A12,FUNCT_1:47,def 3;
      x in succ x by ORDINAL1:6; then
      h.x in h.succ x by A4,A13,ORDINAL2:def 12; then
      g.x in u by A14,TARSKI:def 4; then
      g.a c/= g.x & x in dom g by A3,A11,A12,Th4; then
      a c/= x by A11,Th22;
      hence thesis by Th4;
    end;
    hence thesis by A11;
  end;

registration
  let f be normal Ordinal-Sequence;
  cluster criticals f -> continuous;
  coherence
  proof set g = criticals f;
    let a,b;
    reconsider h = g|a as increasing Ordinal-Sequence by ORDINAL4:15;
    assume
A1: a in dom g & a <> {} & a is limit_ordinal & b = g.a; then
A2: b = Union h by Th39;
    a c= dom g by A1,ORDINAL1:def 2; then
    dom h = a by RELAT_1:62;
    hence b is_limes_of g|a by A1,A2,ORDINAL5:6;
  end;
end;

theorem Th40:
  for f1,f2 being Ordinal-Sequence st f1 c= f2
  holds criticals f1 c= criticals f2
  proof
    let f1,f2 be Ordinal-Sequence;
    assume
A1: f1 c= 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 X = X & On Z = Z by Th28; then
    reconsider X,Z as ordinal-membered set;
    set Y = Z\X;
A3: now let x,y; assume x in X; then
      consider a being Element of dom f1 such that
A4:   x = a & a is_a_fixpoint_of f1;
      assume y 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 assume
A7:     b in dom f1; 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;
      end; then
      dom f1 c= b & x in dom f1 by A4,Th4,ABIAN:def 3;
      hence x in y by A6;
    end;
    X c= Z
    proof
      let x; assume x in X; 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 thesis by A8,A9,A2;
    end; then
    X\/Y = Z by XBOOLE_1:45; then
    criticals f2 = (criticals f1)^numbering Y by A3,Th25;
    hence criticals f1 c= criticals f2 by Th9;
  end;

begin :: Fixpoints in a Universal Set

reserve U,W for Universe;

registration
  let U;
  cluster normal for Ordinal-Sequence of U;
  existence
  proof
    reconsider F = id On U as Ordinal-Sequence of U;
    take F;
    thus thesis;
  end;
end;

definition
  let U,a;
  mode Ordinal-Sequence of a,U is Function of a, On U;
end;

registration
  let U,a;
  cluster -> T-Sequence-like Ordinal-yielding for Ordinal-Sequence of a,U;
  coherence
  proof
    let f be Ordinal-Sequence of a,U;
    thus dom f is ordinal by FUNCT_2:def 1;
    take On U;
    thus thesis by RELAT_1:def 19;
  end;
end;

definition
  let U,a;
  let f be Ordinal-Sequence of a,U;
  let x;
  redefine func f.x -> Ordinal of U;
  coherence
  proof
    per cases by FUNCT_1:def 2;
    suppose
      x in dom f; then
      x in a by FUNCT_2:def 1; then
      f.x in On U by FUNCT_2:5;
      hence thesis by ORDINAL1:def 9;
    end;
    suppose
      f.x = 0;
      hence thesis by CLASSES2:56;
    end;
  end;
end;

theorem Th41:
  a in U implies for f being Ordinal-Sequence of a,U holds Union f in U
  proof assume
A1: a in U;
    let f be Ordinal-Sequence of a,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;
  end;

theorem Th42:
  a in U implies for f being Ordinal-Sequence of a,U holds sup f in U
  proof assume
A1: a in U;
    let f be Ordinal-Sequence of a,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;
  end;

scheme CriticalNumber2
  {U() -> Universe, a() -> Ordinal of U(),
  f() -> Ordinal-Sequence of omega, U(),
  phi(Ordinal) -> Ordinal}:
   a() c= Union f() & phi(Union f()) = Union f() &
   for b st a() c= b & b in U() & phi(b) = b holds Union f() c= b
  provided
A1:  omega in U()
  and
A2: for a st a in U() holds phi(a) in U()
  and
A3:  for a,b st a in b & b in U() holds phi(a) in phi(b)
  and
A4: for a being Ordinal of U() st a is non empty limit_ordinal
    for phi being Ordinal-Sequence
      st dom phi = a & for b st b in a holds phi.b = phi(b)
    holds phi(a) is_limes_of phi
  and
A5:  f().0 = a()
  and
A6:  for a st a in omega holds f().(succ a) = phi(f().a)
  proof
A7:dom f() = omega by FUNCT_2:def 1;
A8: a() in rng f() by A5,A7,FUNCT_1:def 3;
    hence a() c= Union f() by ZFMISC_1:74;
    set phi = f();
A9: now
      defpred P[Ordinal] means $1 in U() & $1 c/= phi($1);
      assume
A10:   ex a st P[a];
      consider a such that
A11:   P[a] and
A12:  for b st P[b] holds a c= b from ORDINAL1:sch 1(A10);
      phi(phi(a)) in phi(a) by A3,A11,ORDINAL1:16; then
      phi(a) c/= phi(phi(a)) by ORDINAL1:5;
      hence contradiction by A2,A11,A12;
    end; then
    a() c= phi(a()); then
A13: a() c< phi(a()) or a() = phi(a()) by XBOOLE_0:def 8;
    per cases by A13,ORDINAL1:11;
    suppose
A14:   phi(a()) = a();
A15:   for a be set st a in omega holds f().a = a()
      proof
        let a be set; assume a in omega; then
        reconsider a as Element of omega;
        defpred P[Nat] means f().$1 = a();
A16:     P[0] by A5;
A17:     now let n be Nat; assume
A18:       P[n];
          n in omega by ORDINAL1:def 12; then
          f().succ n = phi(a()) by A6,A18;
          hence P[n+1] by A14,NAT_1:38;
        end;
        for n being Nat holds P[n] from NAT_1:sch 2(A16,A17); then
        P[a];
        hence thesis;
      end;
      rng f() = {a()}
      proof
        thus rng f() c= {a()}
        proof
          let x be set; assume x in rng f(); then
          consider a being set such that
A19:       a in dom f() & x = f().a by FUNCT_1:def 3;
          x = a() by A15,A19,A7;
          hence thesis by TARSKI:def 1;
        end;
        thus thesis by A8,ZFMISC_1:31;
      end; then
      Union f() = a() by ZFMISC_1:25;
      hence phi(Union f()) = Union f() &
      for b st a() c= b & b in U() & phi(b) = b holds Union f() c= b by A14;
    end;
    suppose
A20:   a() in phi(a());
      deffunc F(Ordinal,Ordinal) = phi($2);
      deffunc G(Ordinal,T-Sequence) = {};
A21:   now let a such that
A22:     succ a in omega;
        a in succ a by ORDINAL1:6;
        hence phi.(succ a) = F(a,phi.a) by A6,A22,ORDINAL1:10;
      end;
A23:   for a st a in omega holds a() c= phi.a & phi.a in phi.succ a
      proof let a; assume a in omega; then
        reconsider a as Element of omega;
        defpred N[Nat] means a() c= phi.$1 & phi.$1 in phi.succ $1;
A24:    N[0] by A20,A5,A6;
A25:    now
          let n be Nat; assume
A26:      N[n];
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
          phi.(n+1) = phi(phi.n) & phi.(n+1+1) = phi(phi.(n+1)) by A21; then
          phi.n c= phi.(n+1) & phi.(n+1) in phi.(n+1+1) by A3,A9,A26,A27;
          hence N[n+1] by A26,NAT_1:38,XBOOLE_1:1;
        end;
        for n being Nat holds N[n] from NAT_1:sch 2(A24,A25); then
        N[a];
        hence thesis;
      end;
      deffunc phi(Ordinal) = phi($1);
      consider fi being Ordinal-Sequence such that
A28:  dom fi = Union phi & for a st a in Union phi holds fi.a = phi(a)
      from ORDINAL2:sch 3;
      1 = succ 0; then
      f().1 = phi(a()) by A5,A6; then
      phi(a()) in rng phi by A7,FUNCT_1:def 3; then
A29:  phi(a()) c= Union phi by ZFMISC_1:74;
A30:   Union phi in U() by A1,Th41;
      now
        let c; assume c in Union phi; then
        consider x being set such that
A31:     x in dom phi & c in phi.x by CARD_5:2;
        reconsider x as Element of omega by A31,FUNCT_2:def 1;
        succ c c= phi.x & phi.x in phi.succ x by A23,A31,ORDINAL1:21; then
        succ c in phi.succ x & succ x in omega by ORDINAL1:12;
        hence succ c in Union phi by A7,CARD_5:2;
      end; then
A32: Union phi is limit_ordinal by ORDINAL1:28; then
A33:  phi(Union phi) is_limes_of fi by A4,A20,A28,A29,A30;
      fi is increasing
      proof
        let a,b;
        assume
A34:    a in b & b in dom fi; then
        fi.a = phi(a) & fi.b = phi(b) & b in U() by A30,A28,ORDINAL1:10;
        hence thesis by A3,A34;
      end; then
A35:  sup fi = lim fi by A20,A28,A29,A32,ORDINAL4:8
      .= phi(Union phi) by A33,ORDINAL2:def 10;
      thus phi(Union phi) c= Union phi
      proof
        let x be Ordinal;
        assume
A36:    x in phi(Union phi);
        reconsider A = x as Ordinal;
        consider b 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 as Ordinal by A38;
        consider z being set such that
A39:    z in dom phi & y in phi.z by A28,A38,CARD_5:2;
        reconsider z as Ordinal by A39;
        set c = phi.z;
        succ z in omega by A7,A39,ORDINAL1:28; then
A40:    phi.succ z = phi(c) & phi.succ z in rng phi & b = phi(y)
        by A7,A21,A28,A38,FUNCT_1:def 3;
        b in phi(c) & phi(c) c= Union phi by A40,A3,A39,ZFMISC_1:74;
        hence thesis by A37,ORDINAL1:12;
      end;
      thus Union f() c= phi(Union f()) by A9,A1,Th41;
      let b; assume
A41:   a() c= b & b in U() & phi(b) = b;
      rng f() c= b
      proof
        let x be set; assume x in rng f(); then
        consider a being set such that
A42:     a in dom f() & x = f().a by FUNCT_1:def 3;
        reconsider a as Element of omega by A42,FUNCT_2:def 1;
        defpred P[Nat] means f().$1 in b;
        a() <> b by A20,A41; then
        a() c< b by A41,XBOOLE_0:def 8; then
A43:     P[0] by A5,ORDINAL1:11;
A44:     now let n be Nat; assume P[n]; then
          phi(f().n) in b & n in omega by A3,A41,ORDINAL1:def 12; then
          f().succ n in b by A6;
          hence P[n+1] by NAT_1:38;
        end;
        for n being Nat holds P[n] from NAT_1:sch 2(A43,A44); then
        P[a];
        hence thesis by A42;
      end; then
      Union f() c= union b & union b c= b by ORDINAL2:5,ZFMISC_1:77;
      hence Union f() c= b by XBOOLE_1:1;
    end;
  end;

Lm1: {} in omega by ORDINAL1:def 11;

scheme CriticalNumber3
  {U() -> Universe, a() -> Ordinal of U(), phi(Ordinal) -> Ordinal}:
  ex a being Ordinal of U() st a() in a & phi(a) = a
  provided
A1: omega in U()
    and
A2: for a st a in U() holds phi(a) in U()
    and
A3: for a,b st a in b & b in U() holds phi(a) in phi(b)
    and
A4: for a being Ordinal of U() st a is non empty limit_ordinal
    for phi being Ordinal-Sequence
      st dom phi = a & for b st b in a holds phi.b = phi(b)
    holds phi(a) is_limes_of phi
  proof assume
A5: not thesis;
    deffunc F(Ordinal,Ordinal) = phi($2);
    deffunc G(Ordinal,T-Sequence) = {};
    consider phi being Ordinal-Sequence such that
A6: dom phi = omega and
A7: {} in omega implies phi.{} = succ a() and
A8: for a st succ a in omega holds phi.(succ a) = F(a,phi.a) and
    for a st a in omega & a <> {} & a is limit_ordinal
    holds phi.a = G(a,phi|a) from ORDINAL2:sch 11;
A9: rng phi c= On U()
    proof
      let y; assume y in rng phi; then
      consider x such that
A10:   x in dom phi & y = phi.x by FUNCT_1:def 3;
      reconsider x as Element of NAT by A6,A10;
      defpred P[Nat] means phi.$1 in On U();
A11:   P[0] by A7,ORDINAL1:def 9;
A12:   P[n] implies P[n+1]
      proof assume P[n]; then
A13:     phi.n in U() by ORDINAL1:def 9;
A14:     n+1 = succ n by NAT_1:38;
        phi.(n+1) = phi(phi.n) & phi(phi.n) in U() by A8,A14,A13,A2;
        hence P[n+1] by ORDINAL1:def 9;
      end;

      P[n] from NAT_1:sch 2(A11,A12); then P[x];
      hence thesis by A10;
    end; then
    reconsider phi as Ordinal-Sequence of omega,U() by A6,FUNCT_2:2;
A15: now
      defpred P[Ordinal] means $1 in U() & $1 c/= phi($1);
      assume
A16:   ex a st P[a];
      consider a such that
A17:   P[a] and
A18:  for b st P[b] holds a c= b from ORDINAL1:sch 1(A16);
      phi(phi(a)) in phi(a) by A3,A17,ORDINAL1:16; then
      phi(a) c/= phi(phi(a)) by ORDINAL1:5;
      hence contradiction by A17,A18,A2;
    end;
A19:now
      let a;
      assume a() in a & a in U(); then
      a c= phi(a) & a <> phi(a) by A5,A15; then
      a c< phi(a) by XBOOLE_0:def 8;
      hence a in phi(a) by ORDINAL1:11;
    end;
A20: for a st a in omega holds a() in phi.a
    proof let a; assume a in omega; then
      reconsider a as Element of omega;
      defpred N[Nat] means a() in phi.$1;
A21:  N[0] by A7,ORDINAL1:6;
A22:  now
        let n be Nat; assume
A23:    N[n];
        n+1 = succ n & n+1 in omega by NAT_1:38; then
        phi.(n+1) = phi(phi.n) by A8; then
        phi.n in phi.(n+1) by A23,A19;
        hence N[n+1] by A23,ORDINAL1:10;
      end;
      for n being Nat holds N[n] from NAT_1:sch 2(A21,A22); then
      N[a];
      hence thesis;
    end;
A24:phi is increasing
    proof
      let a,b;
      assume
A25:  a in b & b in dom phi; then
A26:  ex c st b = a+^c & c <> {} by ORDINAL3:28;
      defpred R[Ordinal] means
      a+^$1 in omega & $1 <> {} implies phi.a in phi.(a+^$1);
A27:  R[{}];
A28:  for c st R[c] holds R[succ c]
      proof
        let c such that
A29:    a+^c in omega & c <> {} implies phi.a in phi.(a+^c) and
A30:    a+^succ c in omega & 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) = phi(d) & d in phi(d) & a+^({} qua Ordinal) = a
        by A8,A19,A30,A31,A20,ORDINAL2:27;
        hence thesis by A29,A30,A31,ORDINAL1:10;
      end;
A32:  for b st b <> {} & b is limit_ordinal & for c st c in b holds R[c]
      holds R[b]
      proof
        let b such that
A33:    b <> {} & b is limit_ordinal and
        for c st c in b holds a+^c in omega & c <> {} implies
        phi.a in phi.(a+^c) and
A34:    a+^b in omega & b <> {};
        a+^b <> {} by A34,ORDINAL3:26; then
        a+^b is limit_ordinal & {} in a+^b by A33,ORDINAL3:8,29;
        hence thesis by A34;
      end;
      for c holds R[c] from ORDINAL2:sch 1(A27,A28,A32);
      hence thesis by A6,A25,A26;
    end;
A35: sup phi in U() by A1,Th42;
    deffunc phi(Ordinal) = phi($1);
    consider fi being Ordinal-Sequence such that
A36: dom fi = sup phi & for a st a in sup phi holds fi.a = phi(a)
     from ORDINAL2:sch 3;
     succ a() 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: phi(sup phi) is_limes_of fi by A35,A4,A36;
     fi is increasing
     proof
       let a,b;
       assume
A39:   a in b & b in dom fi; then
       fi.a = phi(a) & fi.b = phi(b) & b in U() by A35,A36,ORDINAL1:10;
       hence thesis by A3,A39;
     end; then
A40: sup fi = lim fi by A36,A37,ORDINAL4:8
     .= phi(sup phi) by A38,ORDINAL2:def 10;
A41:  sup fi c= sup phi
     proof
       let x be Ordinal;
       assume
A42:   x in sup fi;
       reconsider A = x as Ordinal;
       consider b 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 as Ordinal by A44;
       consider c such that
A45:   c in rng phi & y c= c by A36,A44,ORDINAL2:21;
A46:    c in U() 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 as Ordinal by A47;
       succ z in omega by A6,A47,ORDINAL1:28; then
A48:   phi.succ z = phi(c) & phi.succ z in rng phi & b = phi(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
       phi(y) in phi(c) or y = c by A46,A3,A45,ORDINAL1:11; then
       b c= phi(c) & phi(c) in sup phi by A48,ORDINAL1:def 2,ORDINAL2:19; then
       b in sup phi by ORDINAL1:12;
       hence thesis by A43,ORDINAL1:12;
     end;
     phi.0 in rng phi by A6,FUNCT_1:def 3; then
     a() in phi.0 & phi.0 in sup phi by A20,ORDINAL2:19; then
     a() in sup phi by ORDINAL1:10;
     hence contradiction by A35,A19,A40,A41,ORDINAL1:5;
   end;

reserve F,phi for normal Ordinal-Sequence of W;

theorem Th43:
  omega in W & b in W implies ex a st b in a & a is_a_fixpoint_of phi
  proof assume that
A1: omega in W and
A2: b in W;
    reconsider b1 = b as Ordinal of W by A2;
A3: dom phi = On W by FUNCT_2:def 1;
    deffunc phi(set) = phi.$1;
A4: for a st a in W holds phi(a) in W;
A5: for a,b st a in b & b in W holds phi(a) in phi(b)
    proof
      let a,b;
      b in W implies b in dom phi by A3,ORDINAL1:def 9;
      hence thesis by ORDINAL2:def 12;
    end;
A6: for a being Ordinal of W st a is non empty limit_ordinal
    for f being Ordinal-Sequence
      st dom f = a & for b st b in a holds f.b = phi(b)
    holds phi(a) is_limes_of f
    proof let a be Ordinal of W;
      assume
A7:   a is non empty limit_ordinal;
      let f be Ordinal-Sequence such that
A8:   dom f = a and
A9:   for b st b in a holds f.b = phi(b);
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 let x; assume
A12:     x in a;
        hence (phi|a).x = phi(x) by FUNCT_1:49 .= f.x by A12,A9;
      end; then
      f = phi|a by A8,A11,FUNCT_1:2;
      hence phi(a) is_limes_of f by A7,A10,ORDINAL2:def 13;
    end;
    consider a being Ordinal of W such that
A13: b1 in a & phi(a) = a from CriticalNumber3(A1,A4,A5,A6);
    take a;
    thus b in a & a in dom phi & a = phi.a by A3,A13,ORDINAL1:def 9;
  end;

theorem Th44:
  omega in W implies criticals F is Ordinal-Sequence of W
  proof assume
A1: omega in 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 G c= rng F by Th30; then
A4: rng G c= On W by A2,XBOOLE_1:1;
    dom G = On W
    proof
      thus dom G c= On W by A2,Th32;
      let a; assume a in On W; then
A5:   a in W by ORDINAL1:def 9;
      defpred P[Ordinal] means $1 in W implies $1 in dom G;
      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 G & a0 = G.a1 by A6,Th33;
A8:   P[{}] by A7,ORDINAL1:12,XBOOLE_1:2;
A9:   for a st P[a] holds P[succ a]
      proof
        let a; assume
A10:     P[a] & succ a in W;
A11:     a c= succ a by ORDINAL3:1; then
        G.a in rng G by A10,CLASSES1:def 1,FUNCT_1:def 3; then
        G.a in W by A4,ORDINAL1:def 9; then
        consider b such that
A12:     G.a in b & b is_a_fixpoint_of F by A1,Th43;
        consider c such that
A13:     c in dom G & b = G.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 thesis by A13,ORDINAL1:12;
      end;
A14:   for a st a <> {} & a is limit_ordinal &
      for b st b in a holds P[b] holds P[a]
      proof
        let a such that
A15:     a <> {} & a is limit_ordinal and
A16:     for b st b in a holds P[b] and
A17:     a in W;
        set X = G.:a;
        card X c= card a & card a c= a by CARD_1:8,67; then
        card X c= a by XBOOLE_1:1; then
        card X in W by A17,CLASSES1:def 1; then
        card X in On W by ORDINAL1:def 9; then
A18:     card X in card W by CLASSES2:9;
A19:     X c= rng G by RELAT_1:111; then
A20:     X c= On W by A4,XBOOLE_1:1;
        reconsider u = union X as Ordinal by A19,A4,ORDINAL3:4,XBOOLE_1:1;
        On W c= W by ORDINAL2:7; then
        X c= W by A20,XBOOLE_1:1; then
        X in W by A18,CLASSES1:1; then
        u in W by CLASSES2:59; then
        consider b such that
A21:     u in b & b is_a_fixpoint_of F by A1,Th43;
A22:     a c= dom G
        proof
          let c; assume
A23:       c in a; then
          c in W by A17,ORDINAL1:10;
          hence thesis by A16,A23;
        end;
        now
          let x; assume
A24:       x in a; then
          G.x in X by A22,FUNCT_1:def 6; then
          G.x is Ordinal & G.x c= u by A24,ZFMISC_1:74;
          hence G.x in b by A21,ORDINAL1:12;
        end;
        hence thesis by A15,A22,A21,Th38;
      end;
      P[b] from ORDINAL2:sch 1(A8,A9,A14);
      hence thesis by A5;
    end;
    hence thesis by A3,A2,FUNCT_2:2,XBOOLE_1:1;
  end;

theorem Th45:
  f is normal implies
  for a st a in dom criticals f holds f.a c= (criticals f).a
  proof assume
A1: f is normal;
    set g = criticals f;
A2: dom g c= dom f by Th32;
    defpred P[Ordinal] means $1 in dom g implies f.$1 c= g.$1;
A3: P[{}]
    proof
      assume
      {} in dom g; then
      g.0 is_a_fixpoint_of f by Th29; then
      f.(g.0) = g.0 & g.0 in dom f by ABIAN:def 3;
      hence thesis by A1,ORDINAL4:9,XBOOLE_1:2;
    end;
A4: P[a] implies P[succ a]
    proof assume that
      P[a] and
A5:   succ a in dom g;
      g.succ a is_a_fixpoint_of f by A5,Th29; then
      g.succ a in dom f & f.(g.succ a) = g.succ a by ABIAN:def 3;
      hence f.succ a c= g.succ a by A1,A5,ORDINAL4:9,10;
    end;
A6: for a st a <> {} & a is limit_ordinal & for b st b in a holds P[b]
    holds P[a]
    proof
      let a such that
A7:   a <> {} & a is limit_ordinal and
A8:   for b st b in a holds P[b] and
A9:   a in dom g;
      f.a is_limes_of (f|a) & g.a is_limes_of (g|a)
      by A1,A2,A7,A9,ORDINAL2:def 13; then
A10:   f.a = lim(f|a) & g.a = lim(g|a) by ORDINAL2:def 10;
A11:   f|a is increasing & g|a is increasing by A1,ORDINAL4:15;
A12:   a c= dom f & a c= dom g by A2,A9,ORDINAL1:def 2; then
A13:   dom (f|a) = a & dom (g|a) = a by RELAT_1:62; then
      Union(f|a) is_limes_of (f|a) & Union(g|a) is_limes_of (g|a)
      by A7,A11,ORDINAL5:6; then
A14:   f.a = Union(f|a) & g.a = Union(g|a) by A10,ORDINAL2:def 10;
      let b; assume b in f.a; then
      consider x such that
A15:   x in a & b in (f|a).x by A13,A14,CARD_5:2;
      (f|a).x = f.x & (g|a).x = g.x & f.x c= g.x by A12,A8,A15,FUNCT_1:49;
      hence b in g.a by A15,A13,A14,CARD_5:2;
    end;
    thus P[a] from ORDINAL2:sch 1(A3,A4,A6);
  end;

begin :: Sequences of Sequences of Ordinals

definition
  let U;
  let a,b be Ordinal of U;
  redefine func exp(a,b) -> Ordinal of U;
  coherence
  proof
    per cases by ORDINAL3:8;
    suppose a = 0 & b = 0; then
      exp(a,b) = 1-element_of U by ORDINAL2:43;
      hence thesis;
    end;
    suppose a = 0 & b <> 0;
      hence thesis by ORDINAL4:20;
    end;
    suppose
A1:   0 in a;
      defpred P[Ordinal] means $1 in U implies exp(a,$1) in U;
      exp(a,0) = succ 0 by ORDINAL2:43; then
A2:   P[{}] by CLASSES2:5;
A3:   for b holds P[b] implies P[succ b]
      proof
        let b such that
A4:     P[b] and
A5:     succ b in U;
        b in succ b by ORDINAL1:6; then
        reconsider 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 thesis;
      end;
A6:   for b st b <> {} & b is limit_ordinal & for c st c in b holds P[c]
      holds P[b]
      proof
        let b such that
A7:     b <> {} & b is limit_ordinal and
A8:     for c st c in b holds P[c] and
A9:     b in U;
        deffunc F(Ordinal) = exp(a,$1);
        consider f such that
A10:     dom f = b & for c st c in b holds f.c = F(c) from ORDINAL2:sch 3;
        rng f c= On U
        proof
          let x; assume x in rng f; then
          consider y such that
A11:       y in b & x = f.y by A10,FUNCT_1:def 3;
          reconsider y as Ordinal by A11;
          P[y] & y in U & x = F(y) by A9,A8,A10,A11,ORDINAL1:10;
          hence thesis by ORDINAL1:def 9;
        end; then
        reconsider 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 thesis by A9,Th41;
      end;
      for b holds P[b] from ORDINAL2:sch 1(A2,A3,A6);
      hence thesis;
    end;
  end;
end;

definition
  let U,a such that
AA: a in U;
  func U exp a -> Ordinal-Sequence of U means: Def8:
  for b being Ordinal of U holds it.b = exp(a,b);
  existence
  proof
    reconsider a as Ordinal of U by AA;
    deffunc F(Ordinal of U) = exp(a,$1);
    ex f being Ordinal-Sequence of U st
    for b being Ordinal of U holds f.b = F(b) from ORDINAL4:sch 2;
    hence thesis;
  end;
  uniqueness
  proof let f1,f2 be Ordinal-Sequence of U such 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);
    now
      let x be Element of On U;
      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;
    end;
    hence thesis by FUNCT_2:63;
  end;
end;

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

registration
  let U;
  cluster non trivial finite for Ordinal of U;
  existence
  proof
    succ(1-element_of U) is non trivial by NAT_2:def 1;
    hence thesis;
  end;
end;

registration
  cluster non trivial finite for Ordinal;
  existence
  proof
    2 is non trivial by NAT_2:def 1;
    hence thesis;
  end;
end;

registration
  let U;
  let a be non trivial Ordinal of U;
  cluster U exp a -> normal;
  coherence
  proof set f = U exp a;
A1: dom f = 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
      let b; assume b in dom f; then
      b in U by A1,ORDINAL1:def 9;
      hence f.b = exp(a,b) by Def8;
    end;
    hence f is increasing by A3,ORDINAL5:10;
    let b,c; assume
A5: b in dom f & b <> {} & b is limit_ordinal & c = f.b; then
    b c= dom f by ORDINAL1:def 2; then
A6: dom (f|b) = b by RELAT_1:62;
A7: f|b is increasing by A4,A3,ORDINAL4:15,ORDINAL5:10;
A8: b in U by A1,A5,ORDINAL1:def 9; then
A9: f.b = exp(a,b) by Def8;
    f.b = Union(f|b)
    proof
      thus f.b c= Union(f|b)
      proof
        let c; assume c in f.b; then
        consider d 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) = f.d by Def8 .= (f|b).d by A10,FUNCT_1:49;
        hence c in Union(f|b) by A6,A10,CARD_5:2;
      end;
      let c; assume c in Union(f|b); then
      consider x such that
A11:   x in b & c in (f|b).x by A6,CARD_5:2;
      reconsider x as Ordinal by A11;
      x in U by A8,A11,ORDINAL1:10; then
      exp(a,x) = f.x by Def8 .= (f|b).x by A11,FUNCT_1:49;
      hence thesis by A2,A11,A5,A9,ORDINAL5:11;
    end;
    hence thesis by A5,A7,A6,ORDINAL5:6;
  end;
end;

definition
  let g be Function;
  attr g is Ordinal-Sequence-valued means:
Def9:  x in rng g implies x is Ordinal-Sequence;
end;

registration
  let f be Ordinal-Sequence;
  cluster <%f%> -> Ordinal-Sequence-valued;
  coherence
  proof
    let x; assume x in rng <%f%>; then
    x in {f} by AFINSQ_1:33;
    hence thesis by TARSKI:def 1;
  end;
end;

definition ::: MESFUNC8:def 1 generalized
  let f be Function;
  attr f is with_the_same_dom means
  rng f is with_common_domain;
end;

registration
  let f be Function;
  cluster {f} -> with_common_domain;
  coherence
  proof
    let g,h be Function;
    assume g in {f} & h in {f}; then
    g = f & h = f by TARSKI:def 1;
    hence thesis;
  end;
end;

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

registration
  cluster non empty Ordinal-Sequence-valued with_the_same_dom for T-Sequence;
  existence
  proof
    set f = the Ordinal-Sequence; take <%f%>; thus thesis;
  end;
end;

registration
  let g be Ordinal-Sequence-valued Function;
  let x;
  cluster g.x -> Relation-like Function-like;
  coherence
  proof
    per cases by FUNCT_1:def 2;
    suppose g.x = {};
      hence thesis;
    end;
    suppose x in dom g; then
      g.x in rng g by FUNCT_1:def 3;
      hence thesis by Def9;
    end;
  end;
end;

registration
  let g be Ordinal-Sequence-valued Function;
  let x;
  cluster g.x -> T-Sequence-like Ordinal-yielding;
  coherence
  proof
    per cases by FUNCT_1:def 2;
    suppose g.x = {};
      hence thesis;
    end;
    suppose x in dom g; then
      g.x in rng g by FUNCT_1:def 3;
      hence thesis by Def9;
    end;
  end;
end;

registration
  let g be T-Sequence;
  let a;
  cluster g|a -> T-Sequence-like;
  coherence;
end;

registration
  let g be Ordinal-Sequence-valued Function;
  let X;
  cluster g|X -> Ordinal-Sequence-valued;
  coherence
  proof
    let x;
    rng(g|X) c= rng g by RELAT_1:70;
    hence thesis by Def9;
  end;
end;

registration
  let a,b;
  cluster -> Ordinal-yielding T-Sequence-like for Function of a,b;
  coherence
  proof
    let f be Function of a,b;
    rng f c= b by RELAT_1:def 19;
    hence ex c st rng f c= c;
    b = {} implies f = {};
    hence dom f is ordinal by FUNCT_2:def 1;
  end;
end;

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

reserve g for Ordinal-Sequence-valued T-Sequence;

theorem Th46:
  for g holds
  {a where a is Element of dom(g.0): a in dom(g.0) &
  for f st f in rng g holds a is_a_fixpoint_of f} is ordinal-membered
  proof let g;
    now let x;
      assume x in {a where a is Element of dom(g.0): a in dom(g.0) &
      for f st f in rng g holds a is_a_fixpoint_of f};
      then ex a being Element of dom(g.0) st x = a & a in dom(g.0) &
      for f st f in rng g holds a is_a_fixpoint_of f;
      hence x is ordinal;
    end;
    hence thesis by Th1;
  end;

theorem Th47:
  a in dom g & b in dom criticals g
  implies (criticals g).b is_a_fixpoint_of g.a
  proof
    assume that
A1: a in dom g and
A2: b in dom criticals g;
    set h = criticals g;
    set X = {c where c is Element of dom(g.0): c in dom(g.0) &
    for f st f in rng g holds c is_a_fixpoint_of f};
    X is ordinal-membered by Th46; then
    rng h = X by Th19; then
    h.b in X by A2,FUNCT_1:def 3; then
    consider c being Element of dom(g.0) such that
A3: h.b = c & c in dom(g.0) & for f 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;
  end;

theorem
  x in dom criticals g implies x c= (criticals g).x by ORDINAL4:10;

theorem Th49:
  f in rng g implies dom criticals g c= dom f
  proof assume
A1: f in rng g;
    let x be Ordinal;
    set X = {a where a is Element of dom(g.0): a in dom(g.0) &
    for f st f in rng g holds a is_a_fixpoint_of f};
    assume
A2: x in dom criticals g; then
    (criticals g).x in rng criticals g by FUNCT_1:def 3; then
    (criticals g).x in On X & X is ordinal-membered by Th18,Th46; then
    (criticals g).x in X 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 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 thesis by ORDINAL1:12;
  end;

theorem Th50:
  dom g <> {} & (for c st c in dom g holds b is_a_fixpoint_of g.c) implies
  ex a st a in dom criticals g & b = (criticals g).a
  proof
    reconsider X = {a where a is Element of dom(g.0): a in dom(g.0) &
    for f 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 st c in dom g holds b is_a_fixpoint_of g.c;
    b is_a_fixpoint_of g.0 by A2,A1,ORDINAL3:8; then
A3: b in dom(g.0) by ABIAN:def 3;
    now
      let f; assume f in rng g;
      then ex x st x in dom g & f = g.x by FUNCT_1:def 3;
      hence b is_a_fixpoint_of f by A2;
    end; then
    b in X by A3; then
    b in rng criticals g by Th19; then
    ex x st x in dom criticals g & b = (criticals g).x by FUNCT_1:def 3;
    hence thesis;
  end;

theorem
  dom g <> {} & l c= dom criticals g &
  (for f st f in rng g holds a is_a_fixpoint_of f) &
  (for x st x in l holds (criticals g).x in a)
  implies l in dom criticals g
  proof set h = criticals g;
    assume that
A1: dom g <> {} and
A2: l c= dom h and
A3: for f st f in rng g holds a is_a_fixpoint_of f and
A4: for x st x in l holds h.x in a;
    now
      let c; assume
      c in dom g; then
      g.c in rng g by FUNCT_1:def 3;
      hence a is_a_fixpoint_of g.c by A3;
    end; then
    consider b such that
A5: b in dom h & a = h.b by A1,Th50;
    l c= b
    proof
      let x be Ordinal; assume x in l; then
      x in dom h & h.x in h.b by A2,A4,A5;
      hence x in b by A5,Th23;
    end;
    hence l in dom criticals g by A5,ORDINAL1:12;
  end;

theorem Th52:
  for g st dom g <> {} & for a st a in dom g holds g.a is normal
  holds l in dom criticals g implies
  (criticals g).l = Union ((criticals g)|l)
  proof let F be Ordinal-Sequence-valued T-Sequence such that
A1: dom F <> {};
    set g = criticals F;
    reconsider h = g|l as increasing Ordinal-Sequence by ORDINAL4:15;
    set X = rng h;
    assume
A2: (for a st a in dom F holds F.a is normal) & l in dom g;
A3: now
      let a; set f = F.a;
      assume a in dom F; then
      g.l is_a_fixpoint_of F.a by A2,Th47;
      hence g.l in dom f & f.(g.l) = g.l by ABIAN:def 3;
    end;
A4: l c= dom g by A2,ORDINAL1:def 2; then
A5: dom h = l by RELAT_1:62;
A6: for a,x st a in dom F & x in X holds x is_a_fixpoint_of F.a
    proof
      let a,x; assume
A7:   a in dom F & x in X; then
      consider y such that
A8:   y in dom h & x = h.y by FUNCT_1:def 3;
      x = g.y & y in dom g by A4,A5,A8,FUNCT_1:47;
      hence thesis by A7,Th47;
    end;
    reconsider u = union X as Ordinal;
A9: h <> {} by A5;
    now
      let x; assume x in X; then
      consider y such that
A10:   y in dom h & x = h.y by FUNCT_1:def 3;
      x = g.y & y in dom g by A4,A5,A10,FUNCT_1:47; then
      x in g.l by A2,A5,A10,ORDINAL2:def 12;
      hence x c= g.l by ORDINAL1:def 2;
    end; then
A11: u c= g.l by ZFMISC_1:76;
    now let c; set f = F.c;
      assume
A12:   c in dom F; then
A13:   g.l in dom f by A3; then
A14:   u in dom f by A11,ORDINAL1:12;
A15:   f is normal by A2,A12;
      for x st x in X holds x is_a_fixpoint_of f by A6,A12; then
      u = f.u by A9,A13,A15,Th37,A11,ORDINAL1:12;
      hence u is_a_fixpoint_of f by A14,ABIAN:def 3;
    end; then
    consider a such that
A16: a in dom g & u = g.a by A1,Th50;
    a = l
    proof
      thus a c= l by A2,A16,A11,Th22;
      let x be Ordinal; assume
A17:   x in l; then
A18:   succ x in l by ORDINAL1:28; then
A19:   g.x = h.x & g.succ x = h.succ x & h.succ x in X
      by A5,A17,FUNCT_1:47,def 3;
      x in succ x by ORDINAL1:6; then
      h.x in h.succ x by A5,A18,ORDINAL2:def 12; then
      g.x in u by A19,TARSKI:def 4; then
      g.a c/= g.x & x in dom g by A4,A16,A17,Th4; then
      a c/= x by A16,Th22;
      hence thesis by Th4;
    end;
    hence thesis by A16;
  end;

theorem Th53:
  for g st dom g <> {} & for a st a in dom g holds g.a is normal
  holds criticals g is continuous
  proof
    let g;
    assume A1: dom g <> {};
    assume A2: for a st a in dom g holds g.a is normal;
    set f = criticals g;
    let a,b;
    reconsider h = f|a as increasing Ordinal-Sequence by ORDINAL4:15;
    assume
A3: a in dom f & a <> {} & a is limit_ordinal & b = f.a; then
A4: b = Union h by A1,A2,Th52;
    a c= dom f by A3,ORDINAL1:def 2; then
    dom h = a by RELAT_1:62;
    hence b is_limes_of f|a by A3,A4,ORDINAL5:6;
  end;

theorem Th54:
  for g st dom g <> {} & for a st a in dom g holds g.a is normal
  for a,f 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 such that
A1: dom F <> {} and
A2: for a st a in dom F holds F.a is normal;
    let a,f such that
A3: a in dom criticals F and
A4: f in rng F;
    consider x 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 g c= dom f by A4,Th49;
    defpred P[Ordinal] means $1 in dom g implies f.$1 c= g.$1;
A8: P[{}]
    proof
      assume
      {} in dom g; then
      g.0 is_a_fixpoint_of f by A5,Th47; then
      f.(g.0) = g.0 & g.0 in dom f by ABIAN:def 3;
      hence thesis by A6,ORDINAL4:9,XBOOLE_1:2;
    end;
A9: for a holds P[a] implies P[succ a]
    proof let a such that
      P[a] and
A10:   succ a in dom g;
      g.succ a is_a_fixpoint_of f by A5,A10,Th47; then
      g.succ a in dom f & f.(g.succ a) = g.succ a by ABIAN:def 3;
      hence f.succ a c= g.succ a by A6,A10,ORDINAL4:9,10;
    end;
A11: for a st a <> {} & a is limit_ordinal & for b st b in a holds P[b]
    holds P[a]
    proof
      let a such that
A12:   a <> {} & a is limit_ordinal and
A13:   for b st b in a holds P[b] and
A14:   a in dom g;
      g is continuous by A1,A2,Th53; then
      f.a is_limes_of (f|a) & g.a is_limes_of (g|a)
      by A6,A7,A12,A14,ORDINAL2:def 13; then
A15:   f.a = lim(f|a) & g.a = lim(g|a) by ORDINAL2:def 10;
A16:   f|a is increasing & g|a is increasing by A6,ORDINAL4:15;
A17:   a c= dom f & a c= dom g by A7,A14,ORDINAL1:def 2; then
A18:   dom (f|a) = a & dom (g|a) = a by RELAT_1:62; then
      Union(f|a) is_limes_of (f|a) & Union(g|a) is_limes_of (g|a)
      by A12,A16,ORDINAL5:6; then
A19:   f.a = Union(f|a) & g.a = Union(g|a) by A15,ORDINAL2:def 10;
      let b; assume b in f.a; then
      consider x such that
A20:   x in a & b in (f|a).x by A18,A19,CARD_5:2;
      (f|a).x = f.x & (g|a).x = g.x & f.x c= g.x by A17,A13,A20,FUNCT_1:49;
      hence b in g.a by A20,A18,A19,CARD_5:2;
    end;
    for a holds P[a] from ORDINAL2:sch 1(A8,A9,A11);
    hence thesis by A3;
  end;

theorem Th55:
  for g1,g2 being Ordinal-Sequence-valued T-Sequence
  st dom g1 = dom g2 & dom g1 <> {} & for a 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;
    assume
A1: dom g1 = dom g2;
    assume
A2: dom g1 <> {};
    assume
A3: for a st a in dom g1 holds g1.a c= g2.a;
    set f1 = g1.0, f2 = g2.0;
    0 in dom g1 by A2,ORDINAL3:8; then
    f1 c= f2 & f1 in rng g1 & f2 in rng g2 by A1,A3,FUNCT_1:def 3; then
A4: dom f1 c= dom f2 by GRFUNC_1:2;
    set X = {a where a is Element of dom f1: a in dom f1 &
    for f st f in rng g1 holds a is_a_fixpoint_of f};
    set Z = {a where a is Element of dom f2: a in dom f2 &
    for f st f in rng g2 holds a is_a_fixpoint_of f};
    reconsider X,Z as ordinal-membered set by Th46;
    set Y = Z\X;
A5: now let x,y; assume x in X; then
      consider a being Element of dom f1 such that
A6:   x = a & a in dom f1 & for f st f in rng g1 holds a is_a_fixpoint_of f;
      assume y in Y; then
A7:   y in Z & not y in X by XBOOLE_0:def 5; then
      consider b being Element of dom f2 such that
A8:   y = b & b in dom f2 & for f st f in rng g2 holds b is_a_fixpoint_of f;
      assume not x in y; then
A9:   b c= a by A6,A8,ORDINAL1:16; then
A10:   b in dom f1 by A6,ORDINAL1:12;
      now
        let f; assume
A11:     f in rng g1; then
        consider z 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;
      end;
      hence contradiction by A7,A8,A10;
    end;
    X c= Z
    proof
      let x; assume x in X; then
      consider a being Element of dom f1 such that
A16:   x = a & a in dom f1 & for f st f in rng g1 holds a is_a_fixpoint_of f;
      now let f; assume
        f in rng g2; then
        consider z 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;
      end;
      hence thesis by A16,A4;
    end; then
    X\/Y = Z by XBOOLE_1:45; then
    criticals g2 = (criticals g1)^numbering Y by A5,Th25;
    hence criticals g1 c= criticals g2 by Th9;
  end;

definition
  let g be Ordinal-Sequence-valued T-Sequence;
  func lims g -> Ordinal-Sequence means:
Def12:
  dom it = dom (g.0) & for a st a in dom it holds
  it.a = union {g.b.a where b is Element of dom g: b in dom g};
  existence
  proof
    deffunc X(Ordinal) = {g.b.$1 where b is Element of dom g: b in dom g};
    deffunc F(Ordinal) = union On X($1);
    consider f such that
A1: dom f = dom(g.0) & for a st a in dom(g.0) holds f.a = F(a)
    from ORDINAL2:sch 3;
    take f; thus dom f = dom(g.0) by A1;
    let a; assume a in dom f; then
A2: f.a = F(a) by A1;
    now
      let x; assume x in X(a); then
      ex b being Element of dom g st x = g.b.a & b in dom g;
      hence x is ordinal;
    end; then
    X(a) is ordinal-membered by Th1;
    hence thesis by A2,Th2;
  end;
  uniqueness
  proof
    let f1,f2 be Ordinal-Sequence such that
A3: dom f1 = dom (g.0) & for a 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 st a in dom f2 holds f2.a =
    union {g.b.a where b is Element of dom g: b in dom g};
    thus dom f1 = dom f2 by A3,A4;
    let x; assume
A5: x in dom f1; then
    f1.x = union {g.b.x where b is Element of dom g: b in dom g} by A3;
    hence thesis by A3,A4,A5;
  end;
end;

theorem Th56:
  for g being Ordinal-Sequence-valued T-Sequence
  st dom g <> {} & dom g in U &
  for a st a in dom g holds g.a is Ordinal-Sequence of U
  holds lims g is Ordinal-Sequence of U
  proof
    let g be Ordinal-Sequence-valued T-Sequence;
    assume
A1: dom g <> {} & dom g in U;
    assume
A2: for a st a in dom g holds g.a 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; assume x in rng lims g; then
      consider y such that
A4:   y in dom lims g & x = (lims g).y by FUNCT_1:def 3;
      reconsider y as Ordinal by A4;
      set X = {g.b.y where b is Element of dom g: b in dom g};
A5:   x = union X by A4,Def12;
      reconsider a = dom g as non empty Ordinal of U by A1;
      deffunc F(set) = g.$1.y;
A6:   card {F(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 X c= a by A6,XBOOLE_1:1; then
      card X in U by CLASSES1:def 1; then
      card X in On U by ORDINAL1:def 9; then
A7:   card X in card U by CLASSES2:9;
A8:   X c= On U
      proof
        let z; assume z in X; 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 thesis by ORDINAL1:def 9;
      end; then
      reconsider u = union X as Ordinal by ORDINAL3:4;
      On U c= U by ORDINAL2:7; then
      X c= U by A8,XBOOLE_1:1; then
      X in U by A7,CLASSES1:1; then
      u in U by CLASSES2:59;
      hence thesis by A5,ORDINAL1:def 9;
    end;
    hence lims g is Ordinal-Sequence of U by A3,FUNCT_2:2;
  end;

begin :: Veblen Hierarchy

definition
  let x;
  func OS@ x -> Ordinal-Sequence equals: Def13:
  x if x is Ordinal-Sequence otherwise the Ordinal-Sequence;
  correctness;
  func OSV@ x -> Ordinal-Sequence-valued T-Sequence equals: Def14:
  x if x is Ordinal-Sequence-valued T-Sequence
  otherwise the Ordinal-Sequence-valued T-Sequence;
  correctness;
end;

definition
  let U;
  func U-Veblen -> Ordinal-Sequence-valued T-Sequence means: Def15:
  dom it = On U & it.0 = U exp omega &
  (for b st succ b in On U holds it.succ b = criticals (it.b)) &
  (for l st l in On U holds it.l = criticals (it|l));
  existence
  proof
    reconsider o = omega as non trivial Ordinal;
    deffunc C(set,set) = criticals OS@ $2;
    deffunc D(set,set) = 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 st succ b in On U holds L.(succ b) = C(b,L.b) and
A4: for b st b in On U & b <> {} & b is limit_ordinal holds L.b = D(b,L|b)
    from ORDINAL2:sch 5;
    defpred P[Ordinal] means
    $1 in On U implies L.$1 is Ordinal-Sequence;
A5: P[{}] by A2;
A6: P[b] implies P[succ b]
    proof assume that
A7:   P[b] and
A8:   succ b in On U;
      b in succ b by ORDINAL1:6; then
      reconsider f = L.b as Ordinal-Sequence by A7,A8,ORDINAL1:10;
      L.(succ b) = C(b,f) by A3,A8 .= criticals f by Def13;
      hence thesis;
    end;
A9: for b st b <> {} & b is limit_ordinal & for c st c in b holds P[c]
    holds P[b]
    proof
      let b; assume that
A10:   b <> {} & b is limit_ordinal and
      for c st c in b holds P[c] and
A11:   b in On U;
      L.b = D(b,L|b) by A4,A10,A11;
      hence thesis;
    end;
A12: P[b] from ORDINAL2:sch 1(A5,A6,A9);
    L is Ordinal-Sequence-valued
    proof
      let x; assume x in rng L; then
      ex y st y in dom L & x = L.y by FUNCT_1:def 3;
      hence thesis by A1,A12;
    end; then
    reconsider L as Ordinal-Sequence-valued T-Sequence;
    take 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;
    hereby
      let b; assume
A13:   succ b in On U;
      reconsider f = L.b as Ordinal-Sequence;
      thus L.succ b = C(b,f) by A13,A3 .= criticals (L.b) by Def13;
    end;
    let l; assume l in On U;
    hence L.l = D(l,L|l) by A4 .= criticals(L|l) by Def14;
  end;
  uniqueness
  proof let g1,g2 be Ordinal-Sequence-valued T-Sequence such that
A14: dom g1 = On U and
A15: g1.0 = U exp omega and
A16: (for b st succ b in On U holds g1.succ b = criticals (g1.b)) and
A17: (for l 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 st succ b in On U holds g2.succ b = criticals (g2.b)) and
A21: (for l st l in On U holds g2.l = criticals(g2|l));
    deffunc C(set,Ordinal-Sequence) = criticals $2;
    deffunc D(set,Ordinal-Sequence-valued T-Sequence) = criticals $2;
A22: {} in On U implies g1.{} = U exp omega by A15;
A23: for b st succ b in On U holds g1.succ b = C(b,g1.b) by A16;
A24: for a st a in On U & a <> {} & a is limit_ordinal
    holds g1.a = D(a,g1|a) by A17;
A25: {} in On U implies g2.{} = U exp omega by A19;
A26: for b st succ b in On U holds g2.succ b = C(b,g2.b) by A20;
A27: for a st a in On U & a <> {} & a is limit_ordinal
    holds g2.a = D(a,g2|a) by A21;
    thus g1 = g2 from ORDINAL2:sch 4(A14,A22,A23,A24,A18,A25,A26,A27);
  end;
end;

registration
  cluster uncountable for Universe;
  existence
  proof
    take U = Tarski-Class omega;
    omega in U by CLASSES1:2; then
    card omega in card U by CLASSES2:1;
    hence card U c/= omega;
  end;
end;

theorem Th57:
  for U being Universe holds U is uncountable iff omega in U
  proof
    let U be Universe;
    thus U is uncountable implies omega in U
    proof assume
      card U c/= omega; then
      omega in card U by Th4; then
      omega in On U by CLASSES2:9;
      hence omega in U by ORDINAL1:def 9;
    end;
    assume omega in U; then
    card omega in card U by CLASSES2:1;
    hence card U c/= omega;
  end;

theorem Th58:
  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
  proof assume
A1: a in b & b in U & omega in U;
    set F = U-Veblen;
    defpred P[Ordinal] means $1 in U implies
    for a,c st a in $1 & c in dom(F.$1) holds F.$1.c is_a_fixpoint_of F.a;
A2: P[0];
A3: for b st P[b] holds P[succ b]
    proof
      let b such that
A4:   P[b] and
A5:   succ b in U;
A6:   b in succ b by ORDINAL1:6;
      let a,c;
      assume a in succ b; 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:   F.succ b = criticals(F.b) by Def15;
      assume c in dom(F.succ b); then
A9:   F.(succ b).c is_a_fixpoint_of F.b by A8,Th29; then
      F.(succ b).c in dom(F.b) & F.(succ b).c = F.b.(F.(succ b).c)
      by ABIAN:def 3;
      hence thesis by A4,A5,A6,A7,A9,ORDINAL1:10,TARSKI:def 1;
    end;
A10: dom F = On U by Def15;
A11: for b st b <> {} & b is limit_ordinal & for d st d in b holds P[d]
    holds P[b]
    proof
      let b such that
A12:   b <> {} & b is limit_ordinal and
      for d st d in b holds P[d] and
A13:   b in U;
A14:   b in On U by A13,ORDINAL1:def 9; then
A15:   F.b = criticals(F|b) by A12,Def15;
      b c= On U by A14,ORDINAL1:def 2; then
A16:   dom(F|b) = b by A10,RELAT_1:62;
      let a,c; assume
A17:   a in b; then
A18:   F.a = (F|b).a by FUNCT_1:49;
      set g = F|b;
      set X = {z where z is Element of dom(g.0): z in dom(g.0) &
      for f st f in rng g holds z is_a_fixpoint_of f};
      now
        let x; assume x in X; then
        ex a being Element of dom(g.0) st x = a & a in dom(g.0) &
        for f st f in rng g holds a is_a_fixpoint_of f;
        hence x is ordinal;
      end; then
      reconsider X as ordinal-membered set by Th1;
      assume
      c in dom(F.b); then
      F.b.c in rng (F.b) by FUNCT_1:def 3; then
      F.b.c in X by A15,Th19; then
      consider z being Element of dom(g.0) such that
A19:   F.b.c = z & z in dom(g.0) &
      for f st f in rng g holds z is_a_fixpoint_of f;
      F.a in rng g by A16,A18,A17,FUNCT_1:def 3;
      hence thesis by A19;
    end;
    for b holds P[b] from ORDINAL2:sch 1(A2,A3,A11);
    hence thesis by A1;
  end;

theorem
  l in U & (for c st c in l holds a is_a_fixpoint_of U-Veblen.c)
  implies a is_a_fixpoint_of lims(U-Veblen|l)
  proof
    assume
A1: l in U;
    assume
A2: for c st c in l holds a is_a_fixpoint_of U-Veblen.c;
    set F = U-Veblen; set g = F|l;
    set X = {g.d.a where d is Element of dom g: d in dom g};
    set u = union X;
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;
    F.0 = U exp o by Def15; then
    reconsider f0 = F.0 as normal Ordinal-Sequence of U;
A4: f0 = g.0 by FUNCT_1:49,ORDINAL3:8; then
A5: dom lims g = 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 F = On U by Def15;
    l in On U by A1,ORDINAL1:def 9; then
    l c= dom F by A8,ORDINAL1:def 2; then
A9: dom g = l by RELAT_1:62;
    set lg = lims g;
    thus a in dom lims g by A5,A6,ABIAN:def 3;
A10: lg.a = u by A5,A7,Def12;
    {a} = X
    proof
      a in X by A3,A9,A7,A4;
      hence {a} c= X by ZFMISC_1:31;
      let x; assume x in X; then
      consider d being Element of dom g such that
A11:   x = g.d.a & d in dom g;
      g.d = F.d by A11,FUNCT_1:47; then
      a is_a_fixpoint_of g.d by A2,A9; then
      x = a by A11,ABIAN:def 3;
      hence thesis by TARSKI:def 1;
    end;
    hence a = (lims g).a by A10,ZFMISC_1:25;
  end;

theorem Th60:
  a c= b & b in U & omega in U & c in dom(U-Veblen.b) &
  (for c st c in b holds U-Veblen.c is normal)
  implies U-Veblen.a.c c= U-Veblen.b.c
  proof assume
A1: a c= b & b in U & omega in U & c in dom(U-Veblen.b);
    set F = U-Veblen;
    defpred P[Ordinal] means
    for a,c st a c= $1 & $1 in U & c in dom(F.$1) &
    for c st c in $1 holds U-Veblen.c is normal holds F.a.c c= F.$1.c;
A2: P[0];
A3: for b st P[b] holds P[succ b]
    proof
      let b such that
A4:   P[b];
      let a,c such that
A5:   a c= succ b and
A6:   succ b in U and
A7:   c in dom(F.succ b);
      assume
A8:   for c st c in succ b holds U-Veblen.c is normal;
      succ b in On U by A6,ORDINAL1:def 9; then
A9:   F.succ b = criticals (F.b) by Def15; then
A10:   dom(F.succ b) c= dom(F.b) by Th32;
A11:   b in succ b by ORDINAL1:6; then
A12:   b in U by A6,ORDINAL1:10;
      F.b is normal by A8,ORDINAL1:6; then
A13:   F.b.c c= F.succ b.c by A7,A9,Th45;
A14:   for c st c in b holds F.c is normal by A8,A11,ORDINAL1:10;
      per cases by A5,ORDINAL5:1;
      suppose a = succ b;
        hence thesis;
      end;
      suppose a c= b; then
        F.a.c c= F.b.c by A4,A7,A10,A12,A14;
        hence thesis by A13,XBOOLE_1:1;
      end;
    end;
A15: for b st b <> {} & b is limit_ordinal & for d st d in b holds P[d]
    holds P[b]
    proof
      let b;
      assume
A16:   b <> {} & b is limit_ordinal;
      assume for d st d in b holds P[d];
      let a,c;
      assume
A17:   a c= b;
      per cases by A17,XBOOLE_0:def 8;
      suppose a = b;
        hence thesis;
      end;
      suppose
A18:     a c< b; then
A19:     a in b by ORDINAL1:11;
        assume
        b in U; then
A20:     b in On U by ORDINAL1:def 9; then
A21:     F.b = criticals(F|b) by A16,Def15;
        dom F = On U by Def15; then
        b c= dom F by A20,ORDINAL1:def 2; then
A22:     dom(F|b) = b by RELAT_1:62;
        assume
A23:     c in dom(F.b);
       assume
A24:     for c st c in b holds U-Veblen.c is normal;
A25:     now let c; assume c in dom(F|b); then
          c in b & (F|b).c = F.c by A22,FUNCT_1:49;
          hence (F|b).c is normal by A24;
        end;
A26:     (F|b).a in rng(F|b) by A19,A22,FUNCT_1:def 3;
        (F|b).a = F.a by A18,FUNCT_1:49,ORDINAL1:11;
        hence F.a.c c= F.b.c by A19,A21,A22,A23,A25,A26,Th54;
      end;
    end;

    for b holds P[b] from ORDINAL2:sch 1(A2,A3,A15);
    hence thesis by A1;
  end;

theorem Th61:
  l in U & a in U & b in l &
  (for c 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
  proof assume that
A1: l in U and
A2: a in U and
A3: b in l and
A4: for c st c in l holds U-Veblen.c is normal Ordinal-Sequence of U;
    set F = U-Veblen;
    set g = F|l;
    set X = {g.d.a where d is Element of dom g: d in dom g};
    set u = union X;
A5: 0 in l by ORDINAL3:8;
    reconsider f0 = F.0, f = F.b as normal Ordinal-Sequence of U
    by A3,A4,ORDINAL3:8;
A6: f0 = g.0 & f = g.b by A3,FUNCT_1:49,ORDINAL3:8; then
A7: dom lims g = dom f0 by Def12 .= On U by FUNCT_2:def 1;
A8: dom F = On U by Def15;
    l in On U by A1,ORDINAL1:def 9; then
    l c= dom F by A8,ORDINAL1:def 2; then
A9: dom g = l by RELAT_1:62; then
A10: g.b.a in X by A3;
    now
      let c; assume
A11:   c in dom g; then
      g.c = F.c by FUNCT_1:47;
      hence g.c is Ordinal-Sequence of U by A9,A11,A4;
    end; then
    reconsider lg = lims g as Ordinal-Sequence of U by A1,A9,Th56;
A12: a in On U by A2,ORDINAL1:def 9; then
A13: lg.a = u by A7,Def12;
A14: dom f = On U & dom f0 = On U by FUNCT_2:def 1;
A15: for x st x in X ex y st x c= y & y in X & y is_a_fixpoint_of f
    proof let x; assume
A16:   x in X; then
      consider d being Element of dom g such that
A17:   x = g.d.a & d in dom g;
      reconsider f2 = F.d as normal Ordinal-Sequence of U by A4,A9;
A18:   f2 = g.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 st c in b holds U-Veblen.c is normal by A4,A3,ORDINAL1:10;
      per cases by ORDINAL1:16;
      suppose
        d c= b; then
A23:     x c= g.b.a by A12,A6,A14,A17,A18,A20,A21,A22,Th60;
        take y = g.(succ b).a;
A24:     b in succ b & succ b in l by A3,ORDINAL1:6,28; then
        reconsider f1 = F.succ b as normal Ordinal-Sequence of U by A4;
A25:     f1 = g.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;
        thus y in X by A9,A24;
        thus thesis by A12,A25,A26,Th29;
      end;
      suppose
A27:     b in d;
        take y = x;
        thus x c= y & y in X by A16;
        thus thesis by A12,A17,A27,A18,A19,A20,Th58;
      end;
    end;
    thus (lims(U-Veblen|l)).a in dom(U-Veblen.b) by A13,A14,ORDINAL1:def 9;
    hence thesis by A13,A10,A15,Th36;
  end;

Lm2:
  omega in U implies U-Veblen.0 is normal Ordinal-Sequence of U
  proof
    assume omega in 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;
  end;

Lm3:
  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
  proof assume that
A1: omega in U and
A2: a in U;
    assume U-Veblen.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;
  end;

Lm4:
  l in U & (for a st a in l holds U-Veblen.a is normal Ordinal-Sequence of U)
  implies U-Veblen.l is normal Ordinal-Sequence of U
  proof
    assume
A1: l in U;
    assume
A2: for a st a in l holds U-Veblen.a 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 = F.l;
A8:   0 in l by ORDINAL3:8;
      reconsider f0 = F.0 as normal Ordinal-Sequence of U by A2,ORDINAL3:8;
A9:   dom f0 = On U by FUNCT_2:def 1;
A10:  f0 = (F|l).0 by FUNCT_1:49,ORDINAL3:8; then
      f0 in rng (F|l) by A6,A8,FUNCT_1:def 3;
      hence dom G c= On U by A4,A9,Th49;
      now
        let c; assume
A11:     c in dom (F|l); then
        (F|l).c = F.c by FUNCT_1:47;
        hence (F|l).c is Ordinal-Sequence of U by A6,A11,A2;
      end; then
      reconsider lg = lims (F|l) as Ordinal-Sequence of U by A1,A6,Th56;
A12:   dom lg = On U by FUNCT_2:def 1;
      rng lg c= rng G
      proof let y;
        assume y in rng lg; then
        consider x such that
A13:     x in dom lg & y = lg.x by FUNCT_1:def 3;
        reconsider 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((F|l).0): a in dom((F|l).0) &
        for f st f in rng(F|l) holds a is_a_fixpoint_of f};
A15:     Y is ordinal-membered by Th46;
        now let f;
          assume f in rng(F|l); then
          consider z such that
A16:       z in l & f = (F|l).z by A6,FUNCT_1:def 3;
          f = F.z by A16,FUNCT_1:49;
          hence y is_a_fixpoint_of f by A1,A2,A16,A13,A14,Th61;
        end; then
        y in Y by A9,A10,A14;
        hence thesis by A4,A15,Th19;
      end; then
A17:   Union lg c= Union G by ZFMISC_1:77;
      On U c= Union lg
      proof
        let a; assume
A18:     a in On U;
A19:     a in succ a by ORDINAL1:6;
        set X = {(F|l).b.succ a where b is Element of dom(F|l):b in dom(F|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 X by A12,Def12;
A22:     f0.succ a in X 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 thesis by A12,A20,CARD_5:2;
      end; then
A24:   On U c= Union G by A17,XBOOLE_1:1;
A25:   rng G c= U
      proof let x;
        assume x in rng G; then
        consider y such that
A26:     y in dom G & x = G.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 thesis;
      end;
      assume On U c/= dom G; then
      dom G in On U by ORDINAL1:16; then
      reconsider d = dom G as Ordinal of U by ORDINAL1:def 9;
A27:   card d in card U by CLASSES2:1;
      card rng G c= card d by CARD_1:12; then
      card rng G in card U by A27,ORDINAL1:12; then
      reconsider r = rng G as Element of U by A25,CLASSES1:1;
      union r in U; then
      Union G in On U by ORDINAL1:def 9; then
      Union G in Union G by A24;
      hence thesis;
    end;
A28: rng (U-Veblen.l) c= On U
    proof
      let x; assume x in rng(U-Veblen.l); then
      consider y such that
A29:   y in dom (U-Veblen.l) & x = (U-Veblen.l).y by FUNCT_1:def 3;
      reconsider 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 thesis by FUNCT_2:def 1;
    end;
    now let a;
      assume
A31:   a in l; then
      (U-Veblen|l).a = U-Veblen.a by FUNCT_1:49;
      hence (U-Veblen|l).a is normal by A2,A31;
    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;
  end;

theorem Th62:
  omega in U & a in U implies U-Veblen.a is normal Ordinal-Sequence of U
  proof assume
A1: omega in U;
    defpred P[Ordinal] means
    $1 in U implies U-Veblen.$1 is normal Ordinal-Sequence of U;
A2: P[0] by A1,Lm2;
A3: P[b] implies P[succ b]
    proof
      b in succ b by ORDINAL1:6;
      then succ b in U implies b in U by ORDINAL1:10;
      hence thesis by A1,Lm3;
    end;
A4: b <> {} & b is limit_ordinal & (for c st c in b holds P[c]) implies P[b]
    proof assume that
A5:   b <> {} & b is limit_ordinal and
A6:   for c st c in b holds P[c] and
A7:   b in U;
      now
        let a; assume
A8:     a in b;
        then a in U by A7,ORDINAL1:10;
        hence U-Veblen.a is normal Ordinal-Sequence of U by A6,A8;
      end;
      hence thesis by A5,A7,Lm4;
    end;
    P[b] from ORDINAL2:sch 1(A2,A3,A4);
    hence thesis;
  end;

theorem Th63:
  omega in U & U c= W & a in U implies U-Veblen.a c= W-Veblen.a
  proof assume
A1: omega in U & U c= W; then
A2: On U c= On W by ORDINAL2:9;
    defpred P[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 let x; assume
      x in On U; 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;
    end; then
A5: P[0] by A2,A3,A4,GRFUNC_1:2;
A6: P[b] implies P[succ b]
    proof assume
A7:   P[b]; assume
A8:   succ b in U;
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 thesis by A7,A9,Th40,A8,ORDINAL1:10;
    end;
A10: b <> {} & b is limit_ordinal & (for c st c in b holds P[c]) implies P[b]
    proof assume that
A11:   b <> {} & b is limit_ordinal and
A12:   for c st c in b holds P[c] and
A13:   b in U;
      set g1 = U-Veblen|b, 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 g1 & W-Veblen.b = criticals g2 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 g1 = b & dom g2 = b by RELAT_1:62;
      now
        let a; assume
A17:     a in dom g1; then
A18:     g1.a = U-Veblen.a & g2.a = W-Veblen.a by A16,FUNCT_1:47;
        a in U by A13,A16,A17,ORDINAL1:10;
        hence g1.a c= g2.a by A12,A16,A17,A18;
      end;
      hence thesis by A11,A15,A16,Th55;
    end;
    P[b] from ORDINAL2:sch 1(A5,A6,A10);
    hence thesis;
  end;

theorem Th64:
  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
  proof assume
A1: omega in U & a in U & b in U & omega in W & a in W & b in W; 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 thesis by A2,A3,GRFUNC_1:2;
  end;

theorem
  l in U & (for a st a in l holds
  U-Veblen.a is normal Ordinal-Sequence of U)
  implies lims(U-Veblen|l) is non-decreasing continuous Ordinal-Sequence of U
  proof set G = U-Veblen;
    assume that
A1: l in U and
A2: for a st a in l holds G.a is normal 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: G.l = criticals(G|l) & dom G = On U by Def15;
    l c= On U by A3,ORDINAL1:def 2; then
A5: dom(G|l) = l by A4,RELAT_1:62;
    set g = G|l;
    now let a; assume
A6:   a in dom g; then
      g.a = G.a by A5,FUNCT_1:49;
      hence g.a is Ordinal-Sequence of U by A2,A5,A6;
    end; then
    reconsider f = lims g as Ordinal-Sequence of U by A1,A5,Th56;
    g.0 = G.0 by FUNCT_1:49,ORDINAL3:8; then
    reconsider g0 = g.0 as Ordinal-Sequence of U by A2,ORDINAL3:8;
A7: dom f = On U by FUNCT_2:def 1;
    deffunc X(set) = {g.b.$1 where b is Element of dom g: b in dom g};
A8: f is non-decreasing
    proof
      let a,b; assume
A9:   a in b & b in dom f; then
      a in dom f by ORDINAL1:10; then
A10:   f.a = union X(a) & f.b = union X(b) by A9,Def12;
      let c; assume c in f.a; then
      consider x such that
A11:   c in x & x in X(a) by A10,TARSKI:def 4;
      consider xa being Element of dom g such that
A12:   x = g.xa.a & xa in dom g by A11;
      g.xa = G.xa by A5,FUNCT_1:49; then
      reconsider h = g.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 X(b) by A11,A12;
      hence c in f.b by A10,TARSKI:def 4;
    end;
    f is continuous
    proof let a,b; assume
A13:   a in dom f & a <> {} & a is limit_ordinal & b = f.a; then
A14:   b = union X(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)
        proof
          let c; assume c in b; then
          consider x such that
A18:       c in x & x in X(a) by A14,TARSKI:def 4;
          consider xa being Element of dom g such that
A19:       x = g.xa.a & xa in dom g by A18;
          g.xa = G.xa by A5,FUNCT_1:49; then
          reconsider h = g.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 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 X(y) by A19; then
          c in union X(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 thesis by A16,A24,CARD_5:2;
        end;
        let c; assume c in Union(f|a); then
        consider x 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 X(x) by Def12; then
        consider y such that
A28:     c in y & y in X(x) by A26,A27,TARSKI:def 4;
        consider z being Element of dom g such that
A29:     y = g.z.x & z in dom g by A28;
        g.z = G.z by A5,FUNCT_1:49; then
        reconsider h = g.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 X(a) by A28,A29;
        hence c in b by A14,TARSKI:def 4;
      end;
      f|a is non-decreasing by A8,Th13;
      hence b is_limes_of f|a by A13,A16,A17,ORDINAL5:6;
    end;
    hence thesis by A8;
  end;

registration
  let a;
  cluster Tarski-Class(a \/ omega) -> uncountable;
  coherence
  proof
    set U = Tarski-Class(a \/ omega);
    omega c= a \/ omega & a \/ omega in U by CLASSES1:2,XBOOLE_1:7; then
    omega in U by CLASSES1:def 1;
    hence thesis by Th57;
  end;
end;

definition
  let a,b;
  func a-Veblen(b) -> Ordinal equals
  (Tarski-Class(a \/ b \/ omega))-Veblen.a.b;
  coherence;
end;

definition
  let n,b;
  redefine func n-Veblen(b) -> Ordinal equals
  (Tarski-Class(b \/ omega))-Veblen.n.b;
  coherence;
  compatibility
  proof
    n c= omega; then
    n\/omega = omega by XBOOLE_1:12;
    hence thesis by XBOOLE_1:4;
  end;
end;

theorem Th66:
  a in Tarski-Class(a\/b\/c)
  proof 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 U by CLASSES1:2,XBOOLE_1:1;
    hence thesis by CLASSES1:def 1;
  end;

theorem Th67:
  omega in U & a in U & b in U implies b-Veblen a = U-Veblen.b.a
  proof assume
A1: omega in U & a in U & b in U;
    set W = Tarski-Class(b\/a\/omega);
    omega in W & a in W & b in W by Th57,Th66;
    hence b-Veblen a = U-Veblen.b.a by A1,Th64;
  end;

theorem Th68:
  0-Veblen(a) = exp(omega,a)
  proof
    set b = 0\/a\/omega;
    set U = Tarski-Class b;
    b in U by CLASSES1:2; then
A1: b in On U by ORDINAL1:def 9;
    omega in On U by A1,ORDINAL1:12,XBOOLE_1:7; then
A2: omega in U by ORDINAL1:def 9;
    a in On U by A1,ORDINAL1:12,XBOOLE_1:7; then
A3: a in U by ORDINAL1:def 9;
    thus 0-Veblen(a) = (U exp omega).a by Def15
    .= exp(omega,a) by A3,A2,Def8;
  end;

theorem Th69:
  b-Veblen((succ b)-Veblen a) = (succ b)-Veblen a
  proof set U = Tarski-Class(b\/a\/omega);
A1: omega in U by Th57;
    reconsider b1 = b as Ordinal of U by Th66;
    succ b1 in On U by ORDINAL1:def 9; then
A2: U-Veblen.(succ b) = criticals (U-Veblen.b) by Def15;
    reconsider f = U-Veblen.b1, g = U-Veblen.(succ b1) as
    normal Ordinal-Sequence of U by A1,Th62;
A3: a in U by Th66; then
A4: a in On U by ORDINAL1:def 9;
A5: dom f = On U & dom g = On U by FUNCT_2:def 1;
    set W = Tarski-Class(b\/(g.a)\/omega);
    omega in U 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 U-Veblen.b by A4,A2,A5,Th29;
    hence b-Veblen((succ b)-Veblen a) = (succ b)-Veblen a by A6,ABIAN:def 3;
  end;

theorem Th70:
  b in c implies b-Veblen(c-Veblen a) = c-Veblen a
  proof assume
A1: b in c;
    set U = Tarski-Class(c\/a\/omega);
A2: omega in U by Th57;
A3: a in U & c in U by Th66; then
A4: b in U by A1,ORDINAL1:10; then
    reconsider f = U-Veblen.b, g = U-Veblen.c as normal Ordinal-Sequence of U
    by A2,Th66,Th62;
    dom g = On U 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;
  end;

theorem Th71:
  a c= b iff c-Veblen a c= c-Veblen b
  proof
    set U = Tarski-Class(c\/b\/omega);
    set W = Tarski-Class(c\/a\/omega);
A1: n in omega & omega in U & omega in W by Th57,ORDINAL1:def 12;
A2: b in U & c in U by Th66;
A3: a in W & c in W by Th66;
    reconsider f = U-Veblen.c as increasing Ordinal-Sequence of U
    by A1,Th66,Th62;
    reconsider g = W-Veblen.c as increasing Ordinal-Sequence of W
    by A1,Th66,Th62;
A4: dom f = On U & dom g = On W by FUNCT_2:def 1;
A5: b in On U & a in On W by A2,A3,ORDINAL1:def 9;
    hereby
      assume
A6:   a c= b; then
A7:   a in U by A2,CLASSES1:def 1;
      per cases by A6,XBOOLE_0:def 8;
      suppose a = b;
        hence c-Veblen a c= c-Veblen b;
      end;
      suppose a c< 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;
      end;
    end;
    assume
A8: c-Veblen a c= c-Veblen b & a c/= b; then
A9: b in a by ORDINAL1:16; then
A10: b in W 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 thesis;
  end;

theorem Th72:
  a in b iff c-Veblen a in c-Veblen b
  proof
    b c= a iff c-Veblen b c= c-Veblen a by Th71;
    hence thesis by Th4;
  end;

theorem
  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
      hereby
        assume
A1:     a-Veblen b in c-Veblen d;
        per cases by ORDINAL1:14;
        case a = c;
          hence b in d by A1,Th72;
        end;
        case a in c; then
          a-Veblen(c-Veblen d) = c-Veblen d by Th70;
          hence b in c-Veblen d by A1,Th72;
        end;
        case c in a; then
          c-Veblen(a-Veblen b) = a-Veblen b by Th70;
          hence a-Veblen b in d by A1,Th72;
        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;
      per cases by A2;
      suppose a = c & b in d;
        hence a-Veblen b in c-Veblen d by Th72;
      end;
      suppose
A3:     a in c & 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;
      end;
      suppose
A4:     c in a & a-Veblen b in d; then
        c-Veblen(a-Veblen b) = a-Veblen b by Th70;
        hence a-Veblen b in c-Veblen d by A4,Th72;
      end;
    end;

begin :: Epsilon Numbers

reserve U for uncountable Universe;

theorem Th74:
  U-Veblen.1 = criticals(U exp omega)
  proof set o = succ(0-element_of U);
    o in On U by ORDINAL1:def 9; then
    U-Veblen.1 = criticals(U-Veblen.0) by Def15;
    hence thesis by Def15;
  end;

theorem Th75:
  1-Veblen(a) is epsilon
  proof 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;
  end;

theorem Th76:
  for e being epsilon Ordinal ex a st e = 1-Veblen a
  proof
    let e be epsilon Ordinal;
    set U = Tarski-Class(e\/omega);
A1: omega in U by Th57;
    0-element_of U = 0 & 1-element_of U = 1; then
    reconsider f = U-Veblen.0, g = U-Veblen.1 as
    normal Ordinal-Sequence of U by A1,Th62;
A2: g = criticals(U 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 U by FUNCT_2:def 1;
    e c= e\/omega & e\/omega in U by CLASSES1:2,XBOOLE_1:7; then
A5: e in U by CLASSES1:def 1; then
    e in On U by ORDINAL1:def 9; then
    e is_a_fixpoint_of f by A3,A4,ABIAN:def 3; then
    consider a such that
A6: a in dom criticals f & e = (criticals f).a by Th33;
    take a;
    set W = Tarski-Class(a\/omega);
A7: a c= a\/omega & a\/omega in W by CLASSES1:2,XBOOLE_1:7;
    a c= e by A6,ORDINAL4:10; then
    omega in W & a in W & a in U & 1-element_of U = 1-element_of W
    by A5,A7,Th57,CLASSES1:def 1;
    hence e = 1-Veblen a by A1,A2,A6,Th64;
  end;

Lm5:
  1-Veblen 0 = epsilon_0
  proof
    consider b such that
A1: 1-Veblen 0 = epsilon_b by Th75,ORDINAL5:51;
    consider a such that
A2: epsilon_0 = 1-Veblen a by Th76;
    now assume b <> 0; then
      epsilon_0 in epsilon_b by ORDINAL3:8,ORDINAL5:44;
      hence contradiction by A1,A2,Th72;
    end;
    hence thesis by A1;
  end;

Lm6:
  1-Veblen a = epsilon_a implies 1-Veblen succ a = epsilon_succ a
  proof
    assume
A1: 1-Veblen a = epsilon_a;
    consider b such that
A2: 1-Veblen succ a = epsilon_b by Th75,ORDINAL5:51;
    consider c 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;
    assume epsilon_succ a c/= 1-Veblen succ a; 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 thesis;
  end;

Lm7:
  (for a st a in l holds 1-Veblen(a) = epsilon_a)
  implies 1-Veblen(l) = epsilon_l
  proof assume
A1: for a st a in l holds 1-Veblen(a) = epsilon_a;
    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 U by CLASSES1:2;
A3: omega in U by Th57;
    1-element_of U = 1; then
    reconsider g = U-Veblen.1 as normal Ordinal-Sequence of U
    by A3,Th62;
    reconsider o = omega as non trivial Ordinal of U by Th57;
    set f = U exp o;
A4: g = criticals f by Th74;
A5: dom g = On U 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 let x;
      assume x in rng(g|l); then
      consider y such that
A9:   y in dom(g|l) & x = (g|l).y by FUNCT_1:def 3;
      reconsider 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 U & 1-element_of U in U 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;
    end;
    hence 1-Veblen(l) c= epsilon_l by A7,ZFMISC_1:76;
    let a; assume a in epsilon_l; then
    consider b 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 thesis by A11,ORDINAL1:10;
  end;

theorem
  1-Veblen(a) = epsilon_a
  proof set U = Tarski-Class(a\/omega);
    defpred P[Ordinal] means 1-Veblen $1 = epsilon_$1;
A1: P[0] by Lm5;
A2: P[b] implies P[succ b] by Lm6;
A3: b <> {} & b is limit_ordinal & (for c st c in b holds P[c]) implies P[b]
    by Lm7;
    P[b] from ORDINAL2:sch 1(A1,A2,A3);
    hence thesis;
  end;