:: Veblen Hierarchy
::  by Grzegorz Bancerek
::
:: Received October 18, 2010
:: Copyright (c) 2010 Association of Mizar Users

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 :SS:
  ex a st X c= a;
end;

registration
  cluster ordinal -> ordinal-membered 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 7;
  end;
end;

theorem EXCH9:
  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
Z1: for x st x in X holds x is ordinal;
    take a = sup X;
    let x; assume
Z2: x in X; then
    x is Ordinal by Z1;
    hence thesis by Z2,ORDINAL2:27;
end;

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

registration
  let X be ordinal-membered set;
  cluster -> ordinal 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 EXCH9;
    end;
  end;
end;

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

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

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

theorem OM0:
  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 EXCH1;
  end;

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

theorem Lem1:
  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
Z0: f is_isomorphism_of RelIncl X, RelIncl Y;
    let x,y such that
Z1: x in X & y in X;
A1: field RelIncl X = X & field RelIncl Y = Y by WELLORD2:def 1; then
    dom f = X & rng f = Y by Z0,WELLORD1:def 7; then
A2: f.x in Y & f.y in Y by Z1,FUNCT_1:def 5;
    x c= y iff [x,y] in RelIncl X by Z1,WELLORD2:def 1; then
    x c= y iff [f.x,f.y] in RelIncl Y by Z0,Z1,A1,WELLORD1:def 7;
    hence thesis by A2,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
Z0: f is_isomorphism_of RelIncl X, RelIncl Y;
    let x,y;
    assume
Z1: 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 Z0,WELLORD1:def 7; then
    f.x in Y & f.y in Y by Z1,FUNCT_1:def 5; then
    reconsider a=f.x,b=f.y,x,y as Ordinal by Z1;
    y c= x iff b c= a by Z0,Z1,Lem1;
    hence thesis by EXCH1;
  end;

theorem Lem3:
  [x,y] in RelIncl X implies x c= y
  proof assume
Z0: [x,y] in RelIncl X;
    field RelIncl X = X by WELLORD2:def 1; then
    x in X & y in X by Z0,RELAT_1:30;
    hence x c= y by Z0,WELLORD2:def 1;
  end;

theorem Lem4:
  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:27;
    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:8;
  end;

theorem ORDINAL4th2:
  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;
X:  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
A5:   x in dom f and
A6:   y = f.x by FUNCT_1:def 5;
      reconsider x as Ordinal by A5;
      per cases;
      suppose
A8:     x in dom f1;
        then
A9:     f1.x in rng f1 by FUNCT_1:def 5;
        y = f1.x by A6,A8,ORDINAL4:def 1;
        hence thesis by A9,XBOOLE_0:def 3;
      end;
      suppose
        not x in dom f1;
        then dom f1 c= x by ORDINAL1:26;
        then
A10:    (dom f1)+^(x-^dom f1) = x by ORDINAL3:def 6;
        then
A11:    x-^dom f1 in dom f2 by X,A5,ORDINAL3:25;
        then y = f2.(x-^dom f1) by A6,A10,ORDINAL4:def 1;
        then y in rng f2 by A11,FUNCT_1:def 5;
        hence thesis by XBOOLE_0:def 3;
      end;
    end;
    let x; assume
A0: x in rng f1 \/ rng f2;
A1: dom f1 c= (dom f1)+^dom f2 by ORDINAL3:27;
    per cases by A0,XBOOLE_0:def 3;
    suppose x in rng f1; then
      consider z such that
A2:   z in dom f1 & x = f1.z by FUNCT_1:def 5;
      x = f.z by A2,ORDINAL4:def 1;
      hence thesis by X,A1,A2,FUNCT_1:def 5;
    end;
    suppose x in rng f2; then
      consider z such that
A2:   z in dom f2 & x = f2.z by FUNCT_1:def 5;
      reconsider z as Ordinal by A2;
A3:   (dom f1)+^z in dom f by X,A2,ORDINAL3:20;
      x = f.((dom f1)+^z) by A2,ORDINAL4:def 1;
      hence thesis by A3,FUNCT_1:def 5;
    end;
  end;

theorem LemE1:
  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:21,ORDINAL5:44;
      hence epsilon_a c= epsilon_b by ORDINAL1:def 2;
    end;
    assume
Z1: epsilon_a c= epsilon_b;
    assume a c/= b; then
    epsilon_b in epsilon_a by ORDINAL1:26,ORDINAL5:44; then
    epsilon_b in epsilon_b by Z1;
    hence thesis;
  end;

theorem LemE2:
  a in b iff epsilon_a in epsilon_b
  proof
    b c/= a iff epsilon_b c/= epsilon_a by LemE1;
    hence thesis by EXCH1;
  end;

registration
  let X be ordinal-membered set;
  cluster union X -> ordinal;
  coherence
  proof
    ex a st X c= a by SS;
    hence thesis by ORDINAL3:6;
  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 8;
  end;
end;

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

registration
  let a;
  cluster id a -> increasing 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,RELAT_1:71,ORDINAL1:19; then
    f.b = b & f.c = c by A1,A2,FUNCT_1:35;
    hence thesis by A2;
  end;
end;

registration
  let a;
  cluster id a -> continuous 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:71; then
A4: c = b by A1,A2,FUNCT_1:35;
    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:35;
    end;
    case c <> {};
      let B,C be Ordinal; assume
B1:   B in c & c in C;
      take D = succ B;
      thus D in dom g by A2,A3,A4,A5,B1,ORDINAL1:41;
      let E be Ordinal; assume
B3:   D c= E & E in dom g; then
      g.E = E by A3,A5,FUNCT_1:35;
      hence B in g.E & g.E in C by A3,A4,A5,B1,B3,ORDINAL1:19,33;
    end;
  end;
end;

registration
  cluster non empty increasing continuous 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: NORM:
  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 NORM;
end;

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

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

theorem ThND:
  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:86; then
    (f|a).b = f.b & (f|a).c = f.c by A2,ORDINAL1:19,FUNCT_1:72;
    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 EXCH10;
end;

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

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

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

theorem
  ord-type {} = 0;

theorem
  ord-type {a} = 1
  proof
    a in succ a by ORDINAL1:10; then
A1: {a} c= succ a by ZFMISC_1:37; then
    order_type_of RelIncl {a} = 1 by CARD_5:49;
    hence thesis by A1,ORDINAL3:8;
  end;

theorem
  a <> b implies ord-type {a,b} = 2
  proof
    assume a <> b; then
A1: card {a,b} = 2 by CARD_2:76;
    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:34; then
A2: {a,b} c= succ(a\/b) by ZFMISC_1:38; then
    On {a,b} = {a,b} by ORDINAL3:8;
    hence thesis by A1,A2,CARD_5:48;
  end;

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

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 SS;
    ex phi being Ordinal-Sequence st phi = f &
    phi is increasing & dom phi = ord-type X & rng phi = On X
    by A1,CARD_5:14;
    hence thesis;
  end;
end;

theorem ThN1:
  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 SS;
    ex phi being Ordinal-Sequence st phi = f &
    phi is increasing & dom phi = ord-type X & rng phi = On X
    by A1,CARD_5:14;
    hence thesis;
  end;

theorem ThN1a:
  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 ThN1 .= X by EXCH10;
  end;

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

theorem ThN3:
  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:50;
    hence thesis by WELLORD1:def 9;
  end;

reserve f for Ordinal-Sequence;

theorem ThN4:
  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 ThN1,ThN3;
    hence thesis by A1,Lem1;
  end;

theorem ThN5:
  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 ThN4;
    hence thesis by A1,EXCH1;
  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 SS;
    ex phi being Ordinal-Sequence st phi = f &
    phi is increasing & dom phi = ord-type X & rng phi = On X
    by A1,CARD_5:14;
    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 SS;
    consider b such that
A2: Y c= b by SS;
    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 SS;
    take a;
    thus thesis by A1,XBOOLE_1:1;
  end;
end;

theorem ThN6:
  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
Z0: 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);
X:  dom(f^g) = (dom f)+^dom g by ORDINAL4:def 1;
A0: dom f = a & dom g = b by ThN1;
A1: rng f = X & rng g = Y by ThN1a;
A2: f is_isomorphism_of RelIncl a, RelIncl On X &
    g is_isomorphism_of RelIncl b, RelIncl On Y by ThN3; then
A3: f is one-to-one & g is one-to-one by WELLORD1:def 7;
    thus
A5: dom(f^g) = (dom f)+^dom g by ORDINAL4:def 1
    .= field R by A0,WELLORD2:def 1;
    thus rng(f^g) = (rng f)\/rng g by ORDINAL4th2
    .= field Q by A1,WELLORD2:def 1; then
A6: rng(f^g) = X\/Y by WELLORD2:def 1;
A7: On X = X & On Y = Y by EXCH10;
    thus f^g is one-to-one
    proof
      let x,y; assume
B1:   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 B1,ORDINAL1:26;
      suppose
B2:     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 A3,B1,B2,FUNCT_1:def 8;
      end;
      suppose
B3:     x in dom f & dom f c= y; then
B4:     (dom f)+^(b-^dom f) = y by ORDINAL3:def 6; then
B5:     b-^dom f in dom g by X,B1,ORDINAL3:25; then
        (f^g).x = f.x & (f^g).y = g.(b-^dom f) by B3,B4,ORDINAL4:def 1; then
        f.x in X & f.x in Y by A1,B1,B3,B5,FUNCT_1:def 5; then
        f.x in f.x by Z0;
        hence thesis;
      end;
      suppose
B3:     dom f c= x & y in dom f; then
B4:     (dom f)+^(a-^dom f) = x by ORDINAL3:def 6; then
B5:     a-^dom f in dom g by X,B1,ORDINAL3:25; then
        (f^g).y = f.y & (f^g).x = g.(a-^dom f) by B3,B4,ORDINAL4:def 1; then
        f.y in X & f.y in Y by A1,B1,B3,B5,FUNCT_1:def 5; then
        f.y in f.y by Z0;
        hence thesis;
      end;
      suppose dom f c= x & dom f c= y; then
B4:     (dom f)+^(a-^dom f) = x & (dom f)+^(b-^dom f) = y
        by ORDINAL3:def 6; then
B5:     a-^dom f in dom g & b-^dom f in dom g by X,B1,ORDINAL3:25; then
        (f^g).y = g.(b-^dom f) & (f^g).x = g.(a-^dom f) by B4,ORDINAL4:def 1;
        hence thesis by A3,B1,B4,B5,FUNCT_1:def 8;
      end;
    end;
    let x,y;
A4: field R = a+^b by WELLORD2:def 1;
    hereby assume
C1:   [x,y] in R;
      hence
C2:   x in field R & y in field R by RELAT_1:30; then
C3:   x c= y by C1,A4,WELLORD2:def 1;
C4:   (f^g).x in X\/Y & (f^g).y in X\/Y by A5,A6,C2,FUNCT_1:def 5;
      thus [(f^g).x,(f^g).y] in Q
      proof
        reconsider x,y as Ordinal by A4,C2;
        per cases by ORDINAL1:26;
        suppose
B2:       x in dom f & y in dom f; then
B6:       [x,y] in RelIncl a by A0,C3,WELLORD2:def 1;
          (f^g).x = f.x & (f^g).y = f.y by B2,ORDINAL4:def 1; then
B7:       [(f^g).x, (f^g).y] in Q1 by A7,A2,B6,WELLORD1:def 7; then
          (f^g).x in field Q1 & (f^g).y in field Q1 by RELAT_1:30; then
          (f^g).x in X & (f^g).y in X by WELLORD2:def 1; then
          (f^g).x c= (f^g).y by B7,WELLORD2:def 1;
          hence thesis by C4,WELLORD2:def 1;
        end;
        suppose
B3:       x in dom f & dom f c= y; then
B4:       (dom f)+^(y-^dom f) = y by ORDINAL3:def 6; then
B5:       y-^dom f in dom g by A0,A4,C2,ORDINAL3:25; then
          (f^g).x = f.x & (f^g).y = g.(y-^dom f) by B3,B4,ORDINAL4:def 1; then
          (f^g).x in X & (f^g).y in Y by A1,B3,B5,FUNCT_1:def 5; then
          (f^g).x in (f^g).y by Z0; then
          (f^g).x c= (f^g).y by ORDINAL1:def 2;
          hence thesis by C4,WELLORD2:def 1;
        end;
        suppose
          dom f c= x & y in dom f; then
          y in x; then
          y in y by C3;
          hence thesis;
        end;
        suppose dom f c= x & dom f c= y; then
B4:       (dom f)+^(x-^dom f) = x & (dom f)+^(y-^dom f) = y
          by ORDINAL3:def 6; then
B5:       x-^dom f in dom g & y-^dom f in dom g by A0,A4,C2,ORDINAL3:25;
          x-^a c= y-^a by C3,ORDINAL3:72; then
B6:       [x-^a,y-^a] in RelIncl b by B5,A0,WELLORD2:def 1;
          (f^g).y = g.(y-^dom f) & (f^g).x = g.(x-^dom f)
          by B4,B5,ORDINAL4:def 1; then
B7:       [(f^g).x, (f^g).y] in Q2 by A7,A0,A2,B6,WELLORD1:def 7; then
          (f^g).x in field Q2 & (f^g).y in field Q2 by RELAT_1:30; then
          (f^g).x in Y & (f^g).y in Y by WELLORD2:def 1; then
          (f^g).x c= (f^g).y by B7,WELLORD2:def 1;
          hence thesis by C4,WELLORD2:def 1;
        end;
      end;
    end;
    assume
D1: x in field R & y in field R & [(f^g).x,(f^g).y] in Q; then
D2: (f^g).x c= (f^g).y by Lem3;
D3: field R1 = a & field R2 = b by WELLORD2:def 1;
    reconsider x,y as Ordinal by A4,D1;
    per cases by ORDINAL1:26;
    suppose
B2:   x in dom f & y in dom f; then
B3:   (f^g).x = f.x & (f^g).y = f.y by ORDINAL4:def 1;
      f.x in X & f.y in X by A1,B2,FUNCT_1:def 5; then
      [f.x, f.y] in Q1 by B3,D2,WELLORD2:def 1; then
      [x,y] in R1 by A7,B2,D3,A0,A2,WELLORD1:def 7; then
      x c= y by Lem3;
      hence thesis by A4,D1,WELLORD2:def 1;
    end;
    suppose
      x in dom f & dom f c= y; then
      x c= y by ORDINAL1:def 2;
      hence thesis by A4,D1,WELLORD2:def 1;
    end;
    suppose
B2:   dom f c= x & y in dom f; then
B3:   (f^g).y = f.y by ORDINAL4:def 1;
B4:   f.y in X by A1,B2,FUNCT_1:def 5;
B7:   (dom f)+^(x-^dom f) = x by B2,ORDINAL3:def 6; then
B5:   x-^dom f in dom g by A0,A4,D1,ORDINAL3:25; then
B6:   (f^g).x = g.(x-^dom f) by B7,ORDINAL4:def 1;
      g.(x-^dom f) in Y by A1,B5,FUNCT_1:def 5; then
      (f^g).y in (f^g).x by B3,B4,B6,Z0; then
      (f^g).y in (f^g).y by D2;
      hence thesis;
    end;
    suppose dom f c= x & dom f c= y; then
B4:   (dom f)+^(x-^dom f) = x & (dom f)+^(y-^dom f) = y
      by ORDINAL3:def 6; then
B5:   x-^dom f in dom g & y-^dom f in dom g by A0,A4,D1,ORDINAL3:25; then
B6:   g.(y-^dom f) in Y & g.(x-^dom f) in Y by A1,FUNCT_1:def 5;
      (f^g).y = g.(y-^dom f) & (f^g).x = g.(x-^dom f)
      by B4,B5,ORDINAL4:def 1; then
      [g.(x-^dom f), g.(y-^dom f)] in Q2
      by B6,D2,WELLORD2:def 1; then
      [(x-^dom f), (y-^dom f)] in R2 by A7,D3,A0,A2,B5,WELLORD1:def 7; then
      x-^dom f c= y-^dom f by Lem3; then
      x c= y by B4,ORDINAL3:21;
      hence thesis by A4,D1,WELLORD2:def 1;
    end;
  end;

theorem ThN7:
  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
Z0: 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);
A0: On(X\/Y) = X\/Y & On X = X & On Y = Y by EXCH10; then
I1: h is_isomorphism_of R,Q by ThN3;
II: f^g is_isomorphism_of P,Q by Z0,ThN6; then
I2: P,Q are_isomorphic & R,Q are_isomorphic by I1,WELLORD1:def 8; then
    Q,R are_isomorphic by WELLORD1:50; then
    a+^b = ord-type(X\/Y) by I2,WELLORD1:52,WELLORD2:11;
    hence numbering(X \/ Y) = (numbering X)^(numbering Y)
    by A0,II,I2,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 ThN7;
    thus ord-type(X \/ Y) = dom numbering(X \/ Y) by ThN1
    .= (dom numbering X)+^(dom numbering Y) by A1,ORDINAL4:def 1
    .= (ord-type X)+^(dom numbering Y) by ThN1
    .= (ord-type X)+^(ord-type Y) by ThN1;
  end;

begin :: Fixpoints of a Normal Function

theorem LemF1:
  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 5;
  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 Th01:
  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 EXCH9;
    hence thesis by EXCH10;
  end;

theorem Th02:
  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 5; then
    g.a in On X by ThN1; then
    g.a in X by Th01; then
    ex b being Element of dom f st g.a = b & b is_a_fixpoint_of f;
    hence thesis;
  end;

theorem Th03:
  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 Th01;
    hence
A1: rng criticals f = X by ThN1;
    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 LemF1;
  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 Th05:
  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 5; then
    (criticals f).x in On X by ThN1; then
    (criticals f).x in X by Th01; 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,ORDINAL4:10,ABIAN:def 3;
    hence thesis by ORDINAL1:22;
  end;

theorem Th06:
  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 Th03; then
    ex x st x in dom criticals f & b = (criticals f).x by FUNCT_1:def 5;
    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
Z0: a in dom g and
Z1: b is_a_fixpoint_of f and
Z2: g.a in b;
    consider c such that
A1: c in dom g & b = g.c by Z1,Th06;
    a in c by Z0,Z2,A1,ThN5; then
    succ a c= c by ORDINAL1:33;
    hence succ a in dom criticals f by A1,ORDINAL1:22;
  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
A0: c in dom g & b = g.c by Th06;
    a in succ a by ORDINAL1:10; then
A3: a in dom g & g.a in g.succ a by A1,ORDINAL1:19,ORDINAL2:def 16;
    On Y = Y by Th01; then
A6: g is_isomorphism_of RelIncl X, RelIncl Y by ThN3;
A7: dom g = X by ThN1;
    b c/= g.a by A1,EXCH1; then
    c c/= a by A0,A3,A6,A7,Lem1; then
    a in c by EXCH1; then
    succ a c= c by ORDINAL1:33;
    hence g.succ a c= b by A0,ORDINAL4:9;
  end;

theorem Th08a:
  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
Z0: f is normal and
Z1: union X in dom f & X is non empty and
Z2: 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 Z1;
    per cases;
    suppose
      ex a st a in X & for b st b in X holds b c= a; then
      consider a such that
A1:   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
A3:     x c= y & y in X & y is_a_fixpoint_of f by Z2;
        y in dom f by A3,ABIAN:def 3; then
        y c= a by A1,A3;
        hence x c= a by A3,XBOOLE_1:1;
      end; then
      union X c= a & a c= union X by A1,ZFMISC_1:92,94; then
A6:   union X = a by XBOOLE_0:def 10; then
      consider y such that
A4:   union X c= y & y in X & y is_a_fixpoint_of f by Z2,A1;
      y in dom f & y = f.y by A4,ABIAN:def 3; then
      y c= union X by A6,A4,A1; then
      y = union X by A4,XBOOLE_0:def 10;
      hence union X = f.union X by A4,ABIAN:def 3;
    end;
    suppose
A3:   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
B0:   y0 c= x0 & x0 in X & x0 is_a_fixpoint_of f by Z1,Z2;
B1:   x0 in dom f by B0,ABIAN:def 3; then
      consider b such that
B2:   b in X & b c/= x0 by B0,A3;
C3:   x0 in b by B1,B2,EXCH1;
      now
        let a; assume a in l; then
        consider x such that
A4:     a in x & x in X by TARSKI:def 4;
        consider y such that
B4:     x c= y & y in X & y is_a_fixpoint_of f by Z2,A4;
A5:     y in dom f by B4,ABIAN:def 3; then
        consider b such that
A6:     b in X & b c/= y by A3,B4;
        succ a c= y & y in b by A4,B4,A5,A6,ORDINAL1:33,EXCH1; then
        succ a in b by ORDINAL1:22;
        hence succ a in l by A6,TARSKI:def 4;
      end; then
      reconsider l as non empty limit_ordinal Ordinal
      by C3,B2,TARSKI:def 4,ORDINAL1:41;
      thus union X c= f.union X by Z1,Z0,ORDINAL4:10;
      reconsider g = f|l as increasing Ordinal-Sequence by Z0,ORDINAL4:15;
      l c= dom f by Z1,ORDINAL1:def 2; then
A9:   dom g = l by RELAT_1:91; then
A7:   Union g is_limes_of g by ORDINAL5:6;
      f.l is_limes_of g by Z0,Z1,ORDINAL2:def 17; then
A8:   f.l = lim g & Union g = lim g by A7,ORDINAL2:def 14;
      let x; assume x in f.union X; then
      consider z such that
C1:   z in dom g & x in g.z by A8,CARD_5:10;
      consider y such that
C2:   z in y & y in X by A9,C1,TARSKI:def 4;
      consider t being set such that
C4:   y c= t & t in X & t is_a_fixpoint_of f by C2,Z2;
C3:   t in dom f & t = f.t by C4,ABIAN:def 3; then
      reconsider z,t as Ordinal by C1;
      f.z = g.z & z in t by C1,C2,C4,FUNCT_1:70; then
      g.z in t by Z0,C3,ORDINAL2:def 16; then
      x in t by C1,ORDINAL1:19;
      hence x in union X by C4,TARSKI:def 4;
    end;
  end;

theorem Th08:
  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
Z0: f is normal and
Z1: union X in dom f & X is non empty and
Z2: 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 Z2;
    hence thesis by Z0,Z1,Th08a;
  end;

theorem Th19:
  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
Z1: l c= dom g and
Z2: a is_a_fixpoint_of f and
Z4: for x st x in l holds g.x in a;
    consider b such that
A1: b in dom g & a = g.b by Z2,Th06;
    l c= b
    proof
      let x be Ordinal; assume x in l; then
      x in dom g & g.x in g.b by Z1,Z4,A1;
      hence x in b by A1,ThN5;
    end;
    hence l in dom criticals f by A1,ORDINAL1:22;
  end;

theorem Th09:
  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
A0: f is normal & l in dom g; then
    g.l is_a_fixpoint_of f by Th02; then
A1: g.l in dom f & f.(g.l) = g.l by ABIAN:def 3;
A2: l c= dom g by A0,ORDINAL1:def 2; then
A3: dom h = l by RELAT_1:91;
A4: 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
B1:   y in dom h & x = h.y by FUNCT_1:def 5;
      x = g.y & y in dom g by A2,A3,B1,FUNCT_1:70;
      hence thesis by Th02;
    end;
    reconsider u = union X as Ordinal;
S5: h <> {} by A3;
    now
      let x; assume x in X; then
      consider y such that
B2:   y in dom h & x = h.y by FUNCT_1:def 5;
      x = g.y & y in dom g by A2,A3,B2,FUNCT_1:70; then
      x in g.l by A0,A3,B2,ORDINAL2:def 16;
      hence x c= g.l by ORDINAL1:def 2;
    end; then
A9: union X c= g.l by ZFMISC_1:94; then
A6: u in dom f by A1,ORDINAL1:22;
    u = f.u by A0,A4,S5,A9,Th08,A1,ORDINAL1:22; then
    u is_a_fixpoint_of f by A6,ABIAN:def 3; then
    consider a such that
A8: a in dom g & u = g.a by Th06;
    a = l
    proof
      thus a c= l by A0,A8,A9,ThN4;
      let x be Ordinal; assume
C1:   x in l; then
C2:   succ x in l by ORDINAL1:41; then
C3:   g.x = h.x & g.succ x = h.succ x & h.succ x in X
      by A3,C1,FUNCT_1:def 5,70;
      x in succ x by ORDINAL1:10; then
      h.x in h.succ x by A3,C2,ORDINAL2:def 16; then
      g.x in u by C3,TARSKI:def 4; then
      g.a c/= g.x & x in dom g by A2,A8,C1,EXCH1; then
      a c/= x by A8,ThN4;
      hence thesis by EXCH1;
    end;
    hence thesis by A8;
  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 Th09;
    a c= dom g by A1,ORDINAL1:def 2; then
    dom h = a by RELAT_1:91;
    hence b is_limes_of g|a by A1,A2,ORDINAL5:6;
  end;
end;

theorem Th0A:
  for f1,f2 being Ordinal-Sequence st f1 c= f2
  holds criticals f1 c= criticals f2
  proof
    let f1,f2 be Ordinal-Sequence;
    assume
Z0: f1 c= f2; then
Z1: dom f1 c= dom f2 by GRFUNC_1:8;
    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 Th01; then
    reconsider X,Z as ordinal-membered set;
    set Y = Z\X;
A1: now let x,y; assume x in X; then
      consider a being Element of dom f1 such that
B1:   x = a & a is_a_fixpoint_of f1;
      assume y in Y; then
B2:   y in Z & not y in X by XBOOLE_0:def 5; then
      consider b being Element of dom f2 such that
B3:   y = b & b is_a_fixpoint_of f2;
      now assume
B4:     b in dom f1; then
        f1.b = f2.b by Z0,GRFUNC_1:8 .= b by B3,ABIAN:def 3; then
        b is_a_fixpoint_of f1 by B4,ABIAN:def 3;
        hence contradiction by B2,B3,B4;
      end; then
      dom f1 c= b & x in dom f1 by B1,EXCH1,ABIAN:def 3;
      hence x in y by B3;
    end;
    X c= Z
    proof
      let x; assume x in X; then
      consider a being Element of dom f1 such that
B1:   x = a & a is_a_fixpoint_of f1;
B6:   a in dom f1 & a = f1.a by B1,ABIAN:def 3; then
      a in dom f2 & a = f2.a by Z0,Z1,GRFUNC_1:8; then
      a is_a_fixpoint_of f2 by ABIAN:def 3;
      hence thesis by B1,B6,Z1;
    end; then
    X\/Y = Z by XBOOLE_1:45; then
    criticals f2 = (criticals f1)^numbering Y by A1,ThN7;
    hence criticals f1 c= criticals f2 by Lem4;
  end;

begin :: Fixpoints in a Universal Set

reserve U,W for Universe;

registration
  let U;
  cluster normal 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 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 4;
    suppose
      x in dom f; then
      x in a by FUNCT_2:def 1; then
      f.x in On U by FUNCT_2:7;
      hence thesis by ORDINAL1:def 10;
    end;
    suppose
      f.x = 0;
      hence thesis by CLASSES2:62;
    end;
  end;
end;

theorem ThC1:
  a in U implies for f being Ordinal-Sequence of a,U holds Union f in U
  proof assume
Z0: 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 Z0,RELAT_1:def 19,CLASSES2:1,CARD_2:80,ORDINAL2:9; then
    card rng f in card U & rng f c= U by XBOOLE_1:1,ORDINAL1:22; then
    rng f in U by CLASSES1:2;
    hence Union f in U by CLASSES2:65;
  end;

theorem ThC2:
  a in U implies for f being Ordinal-Sequence of a,U holds sup f in U
  proof assume
Z0: a in U;
    let f be Ordinal-Sequence of a,U;
    reconsider u = Union f as Ordinal of U by ThC1,Z0;
    On rng f = rng f by EXCH10; then
    sup f c= succ u by ORDINAL3:85;
    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
A0:  omega in U()
  and
P0: for a st a in U() holds phi(a) in U()
  and
A1:  for a,b st a in b & b in U() holds phi(a) in phi(b)
  and
A2: 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
F1:  f().0 = a()
  and
F2:  for a st a in omega holds f().(succ a) = phi(f().a)
  proof
F1a:dom f() = omega by FUNCT_2:def 1;
F0: a() in rng f() by F1,F1a,FUNCT_1:def 5;
    hence a() c= Union f() by ZFMISC_1:92;
    set phi = f();
A7: now
      defpred P[Ordinal] means $1 in U() & $1 c/= phi($1);
      assume
A8:   ex a st P[a];
      consider a such that
A9:   P[a] and
A10:  for b st P[b] holds a c= b from ORDINAL1:sch 1(A8);
      phi(phi(a)) in phi(a) by A1,A9,ORDINAL1:26; then
      phi(a) c/= phi(phi(a)) by ORDINAL1:7;
      hence contradiction by P0,A9,A10;
    end; then
    a() c= phi(a()); then
F3: a() c< phi(a()) or a() = phi(a()) by XBOOLE_0:def 8;
    per cases by F3,ORDINAL1:21;
    suppose
A3:   phi(a()) = a();
A4:   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();
C0:     P[0] by F1;
C1:     now let n be Nat; assume
C2:       P[n];
          n in omega by ORDINAL1:def 13; then
          f().succ n = phi(a()) by F2,C2;
          hence P[n+1] by A3,NAT_1:39;
        end;
        for n being Nat holds P[n] from NAT_1:sch 2(C0,C1); 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
G1:       a in dom f() & x = f().a by FUNCT_1:def 5;
          x = a() by A4,G1,F1a;
          hence thesis by TARSKI:def 1;
        end;
        thus thesis by F0,ZFMISC_1:37;
      end; then
      Union f() = a() by ZFMISC_1:31;
      hence phi(Union f()) = Union f() &
      for b st a() c= b & b in U() & phi(b) = b holds Union f() c= b by A3;
    end;
    suppose
A3:   a() in phi(a());
      deffunc F(Ordinal,Ordinal) = phi($2);
      deffunc G(Ordinal,T-Sequence) = {};
A6:   now let a such that
G1:     succ a in omega;
        a in succ a by ORDINAL1:10;
        hence phi.(succ a) = F(a,phi.a) by F2,G1,ORDINAL1:19;
      end;
B1:   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;
B01:    N[0] by A3,F1,F2;
B02:    now
          let n be Nat; assume
B03:      N[n];
B04:      n+1 = succ n & n+1+1 = succ (n+1) &
          n+1 in omega & n+1+1 in omega by NAT_1:39; then
          phi.(n+1) = phi(phi.n) & phi.(n+1+1) = phi(phi.(n+1)) by A6; then
          phi.n c= phi.(n+1) & phi.(n+1) in phi.(n+1+1) by A1,A7,B03,B04;
          hence N[n+1] by B03,NAT_1:39,XBOOLE_1:1;
        end;
        for n being Nat holds N[n] from NAT_1:sch 2(B01,B02); then
        N[a];
        hence thesis;
      end;
      deffunc phi(Ordinal) = phi($1);
      consider fi being Ordinal-Sequence such that
A23:  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 F1,F2; then
      phi(a()) in rng phi by F1a,FUNCT_1:def 5; then
A24:  phi(a()) c= Union phi by ZFMISC_1:92;
J1:   Union phi in U() by A0,ThC1;
      now
        let c; assume c in Union phi; then
        consider x being set such that
V1:     x in dom phi & c in phi.x by CARD_5:10;
        reconsider x as Element of omega by V1,FUNCT_2:def 1;
        succ c c= phi.x & phi.x in phi.succ x by B1,V1,ORDINAL1:33; then
        succ c in phi.succ x & succ x in omega by ORDINAL1:22;
        hence succ c in Union phi by F1a,CARD_5:10;
      end; then
A249: Union phi is limit_ordinal by ORDINAL1:41; then
A25:  phi(Union phi) is_limes_of fi by A2,A3,A23,A24,J1;
      fi is increasing
      proof
        let a,b;
        assume
A26:    a in b & b in dom fi; then
        fi.a = phi(a) & fi.b = phi(b) & b in U() by J1,A23,ORDINAL1:19;
        hence thesis by A1,A26;
      end; then
A27:  sup fi = lim fi by A3,A23,A24,A249,ORDINAL4:8
      .= phi(Union phi) by A25,ORDINAL2:def 14;
      thus phi(Union phi) c= Union phi
      proof
        let x be Ordinal;
        assume
A28:    x in phi(Union phi);
        reconsider A = x as Ordinal;
        consider b such that
A29:    b in rng fi & A c= b by A27,A28,ORDINAL2:29;
        consider y being set such that
A30:    y in dom fi & b = fi.y by A29,FUNCT_1:def 5;
        reconsider y as Ordinal by A30;
        consider z being set such that
A32:    z in dom phi & y in phi.z by A23,A30,CARD_5:10;
        reconsider z as Ordinal by A32;
        set c = phi.z;
        succ z in omega by F1a,A32,ORDINAL1:41; then
A33:    phi.succ z = phi(c) & phi.succ z in rng phi & b = phi(y)
        by F1a,A6,A23,A30,FUNCT_1:def 5;
        b in phi(c) & phi(c) c= Union phi by A33,ZFMISC_1:92,A1,A32;
        hence thesis by A29,ORDINAL1:22;
      end;
      thus Union f() c= phi(Union f()) by A7,A0,ThC1;
      let b; assume
Z1:   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
Z2:     a in dom f() & x = f().a by FUNCT_1:def 5;
        reconsider a as Element of omega by Z2,FUNCT_2:def 1;
        defpred P[Nat] means f().$1 in b;
        a() <> b by A3,Z1; then
        a() c< b by Z1,XBOOLE_0:def 8; then
Z3:     P[0] by F1,ORDINAL1:21;
Z4:     now let n be Nat; assume P[n]; then
          phi(f().n) in b & n in omega by A1,Z1,ORDINAL1:def 13; then
          f().succ n in b by F2;
          hence P[n+1] by NAT_1:39;
        end;
        for n being Nat holds P[n] from NAT_1:sch 2(Z3,Z4); then
        P[a];
        hence thesis by Z2;
      end; then
      Union f() c= union b & union b c= b by ZFMISC_1:95,ORDINAL2:5;
      hence Union f() c= b by XBOOLE_1:1;
    end;
  end;

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

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
A0: omega in U()
    and
P0: for a st a in U() holds phi(a) in U()
    and
A1: for a,b st a in b & b in U() holds phi(a) in phi(b)
    and
A2: 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
A3: not thesis;
    deffunc F(Ordinal,Ordinal) = phi($2);
    deffunc G(Ordinal,T-Sequence) = {};
    consider phi being Ordinal-Sequence such that
A4: dom phi = omega and
A5: {} in omega implies phi.{} = succ a() and
A6: 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;
K0: rng phi c= On U()
    proof
      let y; assume y in rng phi; then
      consider x such that
K1:   x in dom phi & y = phi.x by FUNCT_1:def 5;
      reconsider x as Element of NAT by A4,K1;
      defpred P[Nat] means phi.$1 in On U();
K2:   P[0] by A5,ORDINAL1:def 10;
K3:   P[n] implies P[n+1]
      proof assume P[n]; then
K5:     phi.n in U() by ORDINAL1:def 10;
K4:     n+1 = succ n by NAT_1:39;
        phi.(n+1) = phi(phi.n) & phi(phi.n) in U() by A6,K4,K5,P0;
        hence P[n+1] by ORDINAL1:def 10;
      end;

      P[n] from NAT_1:sch 2(K2,K3); then P[x];
      hence thesis by K1;
    end; then
    reconsider phi as Ordinal-Sequence of omega,U() by A4,FUNCT_2:4;
A7: now
      defpred P[Ordinal] means $1 in U() & $1 c/= phi($1);
      assume
A8:   ex a st P[a];
      consider a such that
A9:   P[a] and
A10:  for b st P[b] holds a c= b from ORDINAL1:sch 1(A8);
      phi(phi(a)) in phi(a) by A1,A9,ORDINAL1:26; then
      phi(a) c/= phi(phi(a)) by ORDINAL1:7;
      hence contradiction by A9,A10,P0;
    end;
A11:now
      let a;
      assume a() in a & a in U(); then
      a c= phi(a) & a <> phi(a) by A3,A7; then
      a c< phi(a) by XBOOLE_0:def 8;
      hence a in phi(a) by ORDINAL1:21;
    end;
B1: 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;
B01:  N[0] by ORDINAL1:10,A5;
B02:  now
        let n be Nat; assume
B03:    N[n];
        n+1 = succ n & n+1 in omega by NAT_1:39; then
        phi.(n+1) = phi(phi.n) by A6; then
        phi.n in phi.(n+1) by B03,A11;
        hence N[n+1] by B03,ORDINAL1:19;
      end;
      for n being Nat holds N[n] from NAT_1:sch 2(B01,B02); then
      N[a];
      hence thesis;
    end;
A12:phi is increasing
    proof
      let a,b;
      assume
A13:  a in b & b in dom phi; then
A14:  ex c st b = a+^c & c <> {} by ORDINAL3:31;
      defpred R[Ordinal] means
      a+^$1 in omega & $1 <> {} implies phi.a in phi.(a+^$1);
A15:  R[{}];
A16:  for c st R[c] holds R[succ c]
      proof
        let c such that
A17:    a+^c in omega & c <> {} implies phi.a in phi.(a+^c) and
A18:    a+^succ c in omega & succ c <> {};
A19:    a+^c in succ(a+^c) & a+^succ c = succ(a+^c) by ORDINAL1:10,ORDINAL2:45;
        reconsider d = phi.(a+^c) as Ordinal;
        a+^c in omega by A18,A19,ORDINAL1:19; then
        phi.(a+^succ c) = phi(d) & d in phi(d) & a+^({} qua Ordinal) = a
        by A6,A11,A18,A19,ORDINAL2:44,B1;
        hence thesis by A17,A18,A19,ORDINAL1:19;
      end;
A20:  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
A21:    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
A22:    a+^b in omega & b <> {};
        a+^b <> {} by A22,ORDINAL3:29; then
        a+^b is limit_ordinal & {} in a+^b by A21,ORDINAL3:10,32;
        hence thesis by A22;
      end;
      for c holds R[c] from ORDINAL2:sch 1(A15,A16,A20);
      hence thesis by A4,A13,A14;
    end;
J1: sup phi in U() by A0,ThC2;
    deffunc phi(Ordinal) = phi($1);
    consider fi being Ordinal-Sequence such that
A23: 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 A4,A5,Lm1,FUNCT_1:def 5; then
A24: sup phi <> {} & sup phi is limit_ordinal
     by A4,A12,ORDINAL4:16,ORDINAL2:27; then
A25: phi(sup phi) is_limes_of fi by J1,A2,A23;
     fi is increasing
     proof
       let a,b;
       assume
A26:   a in b & b in dom fi; then
       fi.a = phi(a) & fi.b = phi(b) & b in U() by J1,A23,ORDINAL1:19;
       hence thesis by A1,A26;
     end; then
A27: sup fi = lim fi by A23,A24,ORDINAL4:8
     .= phi(sup phi) by A25,ORDINAL2:def 14;
ZZ:  sup fi c= sup phi
     proof
       let x be Ordinal;
       assume
A28:   x in sup fi;
       reconsider A = x as Ordinal;
       consider b such that
A29:   b in rng fi & A c= b by A28,ORDINAL2:29;
       consider y being set such that
A30:   y in dom fi & b = fi.y by A29,FUNCT_1:def 5;
       reconsider y as Ordinal by A30;
       consider c such that
A31:   c in rng phi & y c= c by A23,A30,ORDINAL2:29;
C1:    c in U() by K0,A31,ORDINAL1:def 10;
       consider z being set such that
A32:   z in dom phi & c = phi.z by A31,FUNCT_1:def 5;
       reconsider z as Ordinal by A32;
       succ z in omega by A4,A32,ORDINAL1:41; then
A33:   phi.succ z = phi(c) & phi.succ z in rng phi & b = phi(y)
       by A4,A6,A23,A30,A32,FUNCT_1:def 5;
       y c< c iff y <> c & y c= c by XBOOLE_0:def 8; then
       phi(y) in phi(c) or y = c by C1,A1,A31,ORDINAL1:21; then
       b c= phi(c) & phi(c) in sup phi by A33,ORDINAL1:def 2,ORDINAL2:27; then
       b in sup phi by ORDINAL1:22;
       hence thesis by A29,ORDINAL1:22;
     end;
     phi.0 in rng phi by A4,FUNCT_1:def 5; then
     a() in phi.0 & phi.0 in sup phi by B1,ORDINAL2:27; then
     a() in sup phi by ORDINAL1:19;
     hence contradiction by J1,A11,A27,ZZ,ORDINAL1:7;
   end;

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

theorem Th38:
  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
A0: b in W;
    reconsider b1 = b as Ordinal of W by A0;
A2: dom phi = On W by FUNCT_2:def 1;
    deffunc phi(set) = phi.$1;
P0: for a st a in W holds phi(a) in W;
00: 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 A2,ORDINAL1:def 10;
      hence thesis by ORDINAL2:def 16;
    end;
01: 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
Z0:   a is non empty limit_ordinal;
      let f be Ordinal-Sequence such that
Z1:   dom f = a and
Z2:   for b st b in a holds f.b = phi(b);
A3:   a in dom phi by A2,ORDINAL1:def 10; then
      a c= dom phi by ORDINAL1:def 2; then
A4:   dom (phi|a) = a by RELAT_1:91;
      now let x; assume
A5:     x in a;
        hence (phi|a).x = phi(x) by FUNCT_1:72 .= f.x by A5,Z2;
      end; then
      f = phi|a by Z1,A4,FUNCT_1:9;
      hence phi(a) is_limes_of f by Z0,A3,ORDINAL2:def 17;
    end;
    consider a being Ordinal of W such that
A6: b1 in a & phi(a) = a from CriticalNumber3(A1,P0,00,01);
    take a;
    thus b in a & a in dom phi & a = phi.a by A2,A6,ORDINAL1:def 10;
  end;

theorem Th39:
  omega in W implies criticals F is Ordinal-Sequence of W
  proof assume
A0: omega in W;
    set G = criticals F;
A1: dom F = On W & rng F c= On W by RELAT_1:def 19,FUNCT_2:def 1;
D2: rng G c= rng F by Th03; then
A2: rng G c= On W by A1,XBOOLE_1:1;
    dom G = On W
    proof
      thus dom G c= On W by A1,Th05;
      let a; assume a in On W; then
A3:   a in W by ORDINAL1:def 10;
      defpred P[Ordinal] means $1 in W implies $1 in dom G;
      consider a0 being Ordinal such that
A4:   0-element_of W in a0 & a0 is_a_fixpoint_of F by A0,Th38;
      consider a1 being Ordinal such that
A5:   a1 in dom G & a0 = G.a1 by A4,Th06;
00:   P[{}] by A5,XBOOLE_1:2,ORDINAL1:22;
01:   for a st P[a] holds P[succ a]
      proof
        let a; assume
B1:     P[a] & succ a in W;
B4:     a c= succ a by ORDINAL3:1; then
        G.a in rng G by B1,FUNCT_1:def 5,CLASSES1:def 1; then
        G.a in W by A2,ORDINAL1:def 10; then
        consider b such that
B2:     G.a in b & b is_a_fixpoint_of F by A0,Th38;
        consider c such that
B3:     c in dom G & b = G.c by B2,Th06;
        a in c by B1,B4,B2,B3,ThN5,CLASSES1:def 1; then
        succ a c= c by ORDINAL1:33;
        hence thesis by B3,ORDINAL1:22;
      end;
02:   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
C1:     a <> {} & a is limit_ordinal and
C2:     for b st b in a holds P[b] and
C3:     a in W;
        set X = G.:a;
        card X c= card a & card a c= a by CARD_1:24,CARD_2:3; then
        card X c= a by XBOOLE_1:1; then
        card X in W by C3,CLASSES1:def 1; then
        card X in On W by ORDINAL1:def 10; then
C4:     card X in card W by CLASSES2:10;
D5:     X c= rng G by RELAT_1:144; then
C5:     X c= On W by A2,XBOOLE_1:1;
        reconsider u = union X as Ordinal by D5,A2,XBOOLE_1:1,ORDINAL3:6;
        On W c= W by ORDINAL2:9; then
        X c= W by C5,XBOOLE_1:1; then
        X in W by C4,CLASSES1:2; then
        u in W by CLASSES2:65; then
        consider b such that
B2:     u in b & b is_a_fixpoint_of F by A0,Th38;
C6:     a c= dom G
        proof
          let c; assume
C7:       c in a; then
          c in W by C3,ORDINAL1:19;
          hence thesis by C2,C7;
        end;
        now
          let x; assume
C7:       x in a; then
          G.x in X by C6,FUNCT_1:def 12; then
          G.x is Ordinal & G.x c= u by C7,ZFMISC_1:92;
          hence G.x in b by B2,ORDINAL1:22;
        end;
        hence thesis by C1,C6,B2,Th19;
      end;
      P[b] from ORDINAL2:sch 1(00,01,02);
      hence thesis by A3;
    end;
    hence thesis by D2,A1,XBOOLE_1:1,FUNCT_2:4;
  end;

theorem Th40:
  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 Th05;
    defpred P[Ordinal] means $1 in dom g implies f.$1 c= g.$1;
00: P[{}]
    proof
      assume
      {} in dom g; then
      g.0 is_a_fixpoint_of f by Th02; then
      f.(g.0) = g.0 & g.0 in dom f by ABIAN:def 3;
      hence thesis by A1,XBOOLE_1:2,ORDINAL4:9;
    end;
01: P[a] implies P[succ a]
    proof assume that
      P[a] and
C2:   succ a in dom g;
      g.succ a is_a_fixpoint_of f by C2,Th02; 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,C2,ORDINAL4:9,10;
    end;
02: 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
Z1:   a <> {} & a is limit_ordinal and
Z2:   for b st b in a holds P[b] and
Z3:   a in dom g;
      f.a is_limes_of (f|a) & g.a is_limes_of (g|a)
      by A1,A2,Z1,Z3,ORDINAL2:def 17; then
Z4:   f.a = lim(f|a) & g.a = lim(g|a) by ORDINAL2:def 14;
Z5:   f|a is increasing & g|a is increasing by A1,ORDINAL4:15;
Z9:   a c= dom f & a c= dom g by A2,Z3,ORDINAL1:def 2; then
Z7:   dom (f|a) = a & dom (g|a) = a by RELAT_1:91; then
      Union(f|a) is_limes_of (f|a) & Union(g|a) is_limes_of (g|a)
      by Z1,Z5,ORDINAL5:6; then
Z6:   f.a = Union(f|a) & g.a = Union(g|a) by Z4,ORDINAL2:def 14;
      let b; assume b in f.a; then
      consider x such that
Z8:   x in a & b in (f|a).x by Z7,Z6,CARD_5:10;
      (f|a).x = f.x & (g|a).x = g.x & f.x c= g.x by Z9,Z2,Z8,FUNCT_1:72;
      hence b in g.a by Z8,Z7,Z6,CARD_5:10;
    end;
    thus P[a] from ORDINAL2:sch 1(00,01,02);
  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:10;
    suppose a = 0 & b = 0; then
      exp(a,b) = 1-element_of U by ORDINAL2:60;
      hence thesis;
    end;
    suppose a = 0 & b <> 0;
      hence thesis by ORDINAL4:20;
    end;
    suppose
AA:   0 in a;
      defpred P[Ordinal] means $1 in U implies exp(a,$1) in U;
      exp(a,0) = succ 0 by ORDINAL2:60; then
00:   P[{}] by CLASSES2:6;
01:   for b holds P[b] implies P[succ b]
      proof
        let b such that
A1:     P[b] and
A2:     succ b in U;
        b in succ b by ORDINAL1:10; then
        reconsider b as Ordinal of U by A2,ORDINAL1:19;
        reconsider ab = exp(a,b) as Ordinal of U by A1;
        exp(a,succ b) = a*^ab by ORDINAL2:61;
        hence thesis;
      end;
02:   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
B1:     b <> {} & b is limit_ordinal and
B2:     for c st c in b holds P[c] and
B0:     b in U;
        deffunc F(Ordinal) = exp(a,$1);
        consider f such that
B3:     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
C1:       y in b & x = f.y by B3,FUNCT_1:def 5;
          reconsider y as Ordinal by C1;
          P[y] & y in U & x = F(y) by B0,B2,B3,C1,ORDINAL1:19;
          hence thesis by ORDINAL1:def 10;
        end; then
        reconsider f as Ordinal-Sequence of b,U by B3,FUNCT_2:4;
B4:     exp(a,b) = lim f by B1,B3,ORDINAL2:62;
        f is non-decreasing by AA,B3,ORDINAL5:8; then
        Union f is_limes_of f by B1,B3,ORDINAL5:6; then
        exp(a,b) = Union f by B4,ORDINAL2:def 14;
        hence thesis by B0,ThC1;
      end;
      for b holds P[b] from ORDINAL2:sch 1(00,01,02);
      hence thesis;
    end;
  end;
end;

definition
  let U,a such that
AA: a in U;
  func U exp a -> Ordinal-Sequence of U means: EXP:
  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 10; 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:113;
  end;
end;

registration
  cluster omega -> non trivial;
  coherence
  proof
    0 in omega & 1 in omega;
    hence thesis by ZFMISC_1:def 10;
  end;
end;

registration
  let U;
  cluster non trivial finite 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 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;
A2: a <> 0 & a <> 1 by NAT_2:def 1; then
B2: 0 in a by ORDINAL3:10; then
    succ 0 c= a by ORDINAL1:33; then
    1 c< a by A2,XBOOLE_0:def 8; then
A3: 1 in a by ORDINAL1:21;
S4: now
      let b; assume b in dom f; then
      b in U by A1,ORDINAL1:def 10;
      hence f.b = exp(a,b) by EXP;
    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:91;
S7: f|b is increasing by S4,A3,ORDINAL5:10,ORDINAL4:15;
A8: b in U by A1,A5,ORDINAL1:def 10; then
A9: f.b = exp(a,b) by EXP;
    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
B1:     d in b & c in exp(a,d) by B2,A5,A9,ORDINAL5:11;
        d in U by A8,B1,ORDINAL1:19; then
        exp(a,d) = f.d by EXP .= (f|b).d by B1,FUNCT_1:72;
        hence c in Union(f|b) by A6,B1,CARD_5:10;
      end;
      let c; assume c in Union(f|b); then
      consider x such that
B3:   x in b & c in (f|b).x by A6,CARD_5:10;
      reconsider x as Ordinal by B3;
      x in U by A8,B3,ORDINAL1:19; then
      exp(a,x) = f.x by EXP .= (f|b).x by B3,FUNCT_1:72;
      hence thesis by B2,B3,A5,A9,ORDINAL5:11;
    end;
    hence thesis by A5,S7,A6,ORDINAL5:6;
  end;
end;

definition
  let g be Function;
  attr g is Ordinal-Sequence-valued means:
OSV:  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:36;
    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:36;
    hence rng <%f%> is with_common_domain;
  end;
end;

registration
  cluster non empty Ordinal-Sequence-valued with_the_same_dom 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 4;
    suppose g.x = {};
      hence thesis;
    end;
    suppose x in dom g; then
      g.x in rng g by FUNCT_1:def 5;
      hence thesis by OSV;
    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 4;
    suppose g.x = {};
      hence thesis;
    end;
    suppose x in dom g; then
      g.x in rng g by FUNCT_1:def 5;
      hence thesis by OSV;
    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:99;
    hence thesis by OSV;
  end;
end;

registration
  let a,b;
  cluster -> Ordinal-yielding T-Sequence-like 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 ThA1:
  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 EXCH9;
  end;

theorem ThA2:
  a in dom g & b in dom criticals g
  implies (criticals g).b is_a_fixpoint_of g.a
  proof
    assume that
Z0: a in dom g and
Z1: 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 ThA1; then
    rng h = X by ThN1a; then
    h.b in X by Z1,FUNCT_1:def 5; then
    consider c being Element of dom(g.0) such that
A1: 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 Z0,FUNCT_1:def 5;
    hence (criticals g).b is_a_fixpoint_of g.a by A1;
  end;

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

theorem ThA5:
  f in rng g implies dom criticals g c= dom f
  proof assume
A0: 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
A1: x in dom criticals g; then
    (criticals g).x in rng criticals g by FUNCT_1:def 5; then
    (criticals g).x in On X & X is ordinal-membered by ThN1,ThA1; then
    (criticals g).x in X by EXCH10; then
    consider a being Element of dom(g.0) such that
A2: (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 A0,A2; then
    x c= a & a in dom f & a = f.a by A1,A2,ORDINAL4:10,ABIAN:def 3;
    hence thesis by ORDINAL1:22;
  end;

theorem ThA6:
  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 ThA1;
    assume that
A0: dom g <> {} and
A1: for c st c in dom g holds b is_a_fixpoint_of g.c;
    b is_a_fixpoint_of g.0 by A1,A0,ORDINAL3:10; then
A2: 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 5;
      hence b is_a_fixpoint_of f by A1;
    end; then
    b in X by A2; then
    b in rng criticals g by ThN1a; then
    ex x st x in dom criticals g & b = (criticals g).x by FUNCT_1:def 5;
    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
Z0: dom g <> {} and
Z1: l c= dom h and
Z2: for f st f in rng g holds a is_a_fixpoint_of f and
Z4: 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 5;
      hence a is_a_fixpoint_of g.c by Z2;
    end; then
    consider b such that
A1: b in dom h & a = h.b by Z0,ThA6;
    l c= b
    proof
      let x be Ordinal; assume x in l; then
      x in dom h & h.x in h.b by Z1,Z4,A1;
      hence x in b by A1,ThN5;
    end;
    hence l in dom criticals g by A1,ORDINAL1:22;
  end;

theorem ThA9:
  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
AA: dom F <> {};
    set g = criticals F;
    reconsider h = g|l as increasing Ordinal-Sequence by ORDINAL4:15;
    set X = rng h;
    assume
A0: (for a st a in dom F holds F.a is normal) & l in dom g;
A1: now
      let a; set f = F.a;
      assume a in dom F; then
      g.l is_a_fixpoint_of F.a by A0,ThA2;
      hence g.l in dom f & f.(g.l) = g.l by ABIAN:def 3;
    end;
A2: l c= dom g by A0,ORDINAL1:def 2; then
A3: dom h = l by RELAT_1:91;
A4: for a,x st a in dom F & x in X holds x is_a_fixpoint_of F.a
    proof
      let a,x; assume
B0:   a in dom F & x in X; then
      consider y such that
B1:   y in dom h & x = h.y by FUNCT_1:def 5;
      x = g.y & y in dom g by A2,A3,B1,FUNCT_1:70;
      hence thesis by B0,ThA2;
    end;
    reconsider u = union X as Ordinal;
T5: h <> {} by A3;
    now
      let x; assume x in X; then
      consider y such that
B2:   y in dom h & x = h.y by FUNCT_1:def 5;
      x = g.y & y in dom g by A2,A3,B2,FUNCT_1:70; then
      x in g.l by A0,A3,B2,ORDINAL2:def 16;
      hence x c= g.l by ORDINAL1:def 2;
    end; then
A9: u c= g.l by ZFMISC_1:94;
    now let c; set f = F.c;
      assume
D1:   c in dom F; then
A6:   g.l in dom f by A1; then
A7:   u in dom f by A9,ORDINAL1:22;
D2:   f is normal by A0,D1;
      for x st x in X holds x is_a_fixpoint_of f by A4,D1; then
      u = f.u by T5,A6,D2,Th08,A9,ORDINAL1:22;
      hence u is_a_fixpoint_of f by A7,ABIAN:def 3;
    end; then
    consider a such that
A8: a in dom g & u = g.a by AA,ThA6;
    a = l
    proof
      thus a c= l by A0,A8,A9,ThN4;
      let x be Ordinal; assume
C1:   x in l; then
C2:   succ x in l by ORDINAL1:41; then
C3:   g.x = h.x & g.succ x = h.succ x & h.succ x in X
      by A3,C1,FUNCT_1:def 5,70;
      x in succ x by ORDINAL1:10; then
      h.x in h.succ x by A3,C2,ORDINAL2:def 16; then
      g.x in u by C3,TARSKI:def 4; then
      g.a c/= g.x & x in dom g by A2,A8,C1,EXCH1; then
      a c/= x by A8,ThN4;
      hence thesis by EXCH1;
    end;
    hence thesis by A8;
  end;

theorem ThAA:
  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 Z0: dom g <> {};
    assume Z1: 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
A1: a in dom f & a <> {} & a is limit_ordinal & b = f.a; then
A2: b = Union h by Z0,Z1,ThA9;
    a c= dom f by A1,ORDINAL1:def 2; then
    dom h = a by RELAT_1:91;
    hence b is_limes_of f|a by A1,A2,ORDINAL5:6;
  end;

theorem ThAB:
  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
X0: dom F <> {} and
X1: for a st a in dom F holds F.a is normal;
    let a,f such that
X2: a in dom criticals F and
X3: f in rng F;
    consider x such that
A0: x in dom F & f = F.x by X3,FUNCT_1:def 5;
A1: f is normal by A0,X1;
    set g = criticals F;
A2: dom g c= dom f by X3,ThA5;
    defpred P[Ordinal] means $1 in dom g implies f.$1 c= g.$1;
00: P[{}]
    proof
      assume
      {} in dom g; then
      g.0 is_a_fixpoint_of f by A0,ThA2; then
      f.(g.0) = g.0 & g.0 in dom f by ABIAN:def 3;
      hence thesis by A1,XBOOLE_1:2,ORDINAL4:9;
    end;
01: for a holds P[a] implies P[succ a]
    proof let a such that
      P[a] and
C2:   succ a in dom g;
      g.succ a is_a_fixpoint_of f by A0,C2,ThA2; 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,C2,ORDINAL4:9,10;
    end;
02: 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
Z1:   a <> {} & a is limit_ordinal and
Z2:   for b st b in a holds P[b] and
Z3:   a in dom g;
      g is continuous by X0,X1,ThAA; then
      f.a is_limes_of (f|a) & g.a is_limes_of (g|a)
      by A1,A2,Z1,Z3,ORDINAL2:def 17; then
Z4:   f.a = lim(f|a) & g.a = lim(g|a) by ORDINAL2:def 14;
Z5:   f|a is increasing & g|a is increasing by A1,ORDINAL4:15;
Z9:   a c= dom f & a c= dom g by A2,Z3,ORDINAL1:def 2; then
Z7:   dom (f|a) = a & dom (g|a) = a by RELAT_1:91; then
      Union(f|a) is_limes_of (f|a) & Union(g|a) is_limes_of (g|a)
      by Z1,Z5,ORDINAL5:6; then
Z6:   f.a = Union(f|a) & g.a = Union(g|a) by Z4,ORDINAL2:def 14;
      let b; assume b in f.a; then
      consider x such that
Z8:   x in a & b in (f|a).x by Z7,Z6,CARD_5:10;
      (f|a).x = f.x & (g|a).x = g.x & f.x c= g.x by Z9,Z2,Z8,FUNCT_1:72;
      hence b in g.a by Z8,Z7,Z6,CARD_5:10;
    end;
    for a holds P[a] from ORDINAL2:sch 1(00,01,02);
    hence thesis by X2;
  end;

theorem ThAC:
  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
Z0: dom g1 = dom g2;
    assume
Z1: dom g1 <> {};
    assume
Z2: 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 Z1,ORDINAL3:10; then
    f1 c= f2 & f1 in rng g1 & f2 in rng g2 by Z0,Z2,FUNCT_1:def 5; then
Z4: dom f1 c= dom f2 by GRFUNC_1:8;
    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 ThA1;
    set Y = Z\X;
A1: now let x,y; assume x in X; then
      consider a being Element of dom f1 such that
B1:   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
B2:   y in Z & not y in X by XBOOLE_0:def 5; then
      consider b being Element of dom f2 such that
B3:   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
B4:   b c= a by B1,B3,ORDINAL1:26; then
B5:   b in dom f1 by B1,ORDINAL1:22;
      now
        let f; assume
B7:     f in rng g1; then
        consider z such that
B6:     z in dom g1 & f = g1.z by FUNCT_1:def 5;
B8:     f c= g2.z by Z2,B6;
        g2.z in rng g2 by Z0,B6,FUNCT_1:def 5; then
BB:     b is_a_fixpoint_of g2.z by B3;
        a is_a_fixpoint_of f by B1,B7; then
        a in dom f by ABIAN:def 3; then
B9:     b in dom f by B4,ORDINAL1:22; then
        f.b = g2.z.b by B8,GRFUNC_1:8 .= b by BB,ABIAN:def 3;
        hence b is_a_fixpoint_of f by B9,ABIAN:def 3;
      end;
      hence contradiction by B2,B3,B5;
    end;
    X c= Z
    proof
      let x; assume x in X; then
      consider a being Element of dom f1 such that
B1:   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
B4:     z in dom g2 & f = g2.z by FUNCT_1:def 5;
B5:     g1.z c= f by Z0,Z2,B4; then
B6:     dom(g1.z) c= dom f by GRFUNC_1:8;
        g1.z in rng g1 by Z0,B4,FUNCT_1:def 5; then
        a is_a_fixpoint_of g1.z by B1; then
        a in dom(g1.z) & a = g1.z.a by ABIAN:def 3; then
        a in dom f & a = f.a by B5,B6,GRFUNC_1:8;
        hence a is_a_fixpoint_of f by ABIAN:def 3;
      end;
      hence thesis by B1,Z4;
    end; then
    X\/Y = Z by XBOOLE_1:45; then
    criticals g2 = (criticals g1)^numbering Y by A1,ThN7;
    hence criticals g1 c= criticals g2 by Lem4;
  end;

definition
  let g be Ordinal-Sequence-valued T-Sequence;
  func lims g -> Ordinal-Sequence means:
LIM:
  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 EXCH9;
    hence thesis by A2,EXCH10;
  end;
  uniqueness
  proof
    let f1,f2 be Ordinal-Sequence such that
A1: 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
A2: 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 A1,A2;
    let x; assume
A3: x in dom f1; then
    f1.x = union {g.b.x where b is Element of dom g: b in dom g} by A1;
    hence thesis by A1,A2,A3;
  end;
end;

theorem ThL1:
  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
Z0: dom g <> {} & dom g in U;
    assume
Z1: 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 Z1,Z0,ORDINAL3:10;
Z2: dom lims g = dom g0 by LIM .= 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
A1:   y in dom lims g & x = (lims g).y by FUNCT_1:def 5;
      reconsider y as Ordinal by A1;
      set X = {g.b.y where b is Element of dom g: b in dom g};
A2:   x = union X by A1,LIM;
      reconsider a = dom g as non empty Ordinal of U by Z0;
      deffunc F(set) = g.$1.y;
A3:   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:24; then
      card X c= a by A3,XBOOLE_1:1; then
      card X in U by CLASSES1:def 1; then
      card X in On U by ORDINAL1:def 10; then
C4:   card X in card U by CLASSES2:10;
C5:   X c= On U
      proof
        let z; assume z in X; then
        consider b being Element of a such that
C6:     z = g.b.y & b in a;
        reconsider f = g.b as Ordinal-Sequence of U by Z1;
        z = f.y by C6;
        hence thesis by ORDINAL1:def 10;
      end; then
      reconsider u = union X as Ordinal by ORDINAL3:6;
      On U c= U by ORDINAL2:9; then
      X c= U by C5,XBOOLE_1:1; then
      X in U by C4,CLASSES1:2; then
      u in U by CLASSES2:65;
      hence thesis by A2,ORDINAL1:def 10;
    end;
    hence lims g is Ordinal-Sequence of U by Z2,FUNCT_2:4;
  end;

begin :: Veblen Hierarchy

definition
  let x;
  func OS@ x -> Ordinal-Sequence equals: OSc:
  x if x is Ordinal-Sequence otherwise the Ordinal-Sequence;
  correctness;
  func OSV@ x -> Ordinal-Sequence-valued T-Sequence equals: OSVc:
  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: V:
  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;
00: P[{}] by A2;
01: P[b] implies P[succ b]
    proof assume that
B1:   P[b] and
B2:   succ b in On U;
      b in succ b by ORDINAL1:10; then
      reconsider f = L.b as Ordinal-Sequence by B1,B2,ORDINAL1:19;
      L.(succ b) = C(b,f) by A3,B2 .= criticals f by OSc;
      hence thesis;
    end;
02: 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
C1:   b <> {} & b is limit_ordinal and
      for c st c in b holds P[c] and
C3:   b in On U;
      L.b = D(b,L|b) by A4,C1,C3;
      hence thesis;
    end;
03: P[b] from ORDINAL2:sch 1(00,01,02);
    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 5;
      hence thesis by A1,03;
    end; then
    reconsider L as Ordinal-Sequence-valued T-Sequence;
    take L;
    0-element_of U in On U by ORDINAL1:def 10;
    hence dom L = On U & L.0 = U exp omega by A1,A2;
    hereby
      let b; assume
E1:   succ b in On U;
      reconsider f = L.b as Ordinal-Sequence;
      thus L.succ b = C(b,f) by E1,A3 .= criticals (L.b) by OSc;
    end;
    let l; assume l in On U;
    hence L.l = D(l,L|l) by A4 .= criticals(L|l) by OSVc;
  end;
  uniqueness
  proof let g1,g2 be Ordinal-Sequence-valued T-Sequence such that
01: dom g1 = On U and
A1: g1.0 = U exp omega and
B1: (for b st succ b in On U holds g1.succ b = criticals (g1.b)) and
C1: (for l st l in On U holds g1.l = criticals(g1|l)) and
05: dom g2 = On U and
A2: g2.0 = U exp omega and
B2: (for b st succ b in On U holds g2.succ b = criticals (g2.b)) and
C2: (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;
02: {} in On U implies g1.{} = U exp omega by A1;
03: for b st succ b in On U holds g1.succ b = C(b,g1.b) by B1;
04: for a st a in On U & a <> {} & a is limit_ordinal
    holds g1.a = D(a,g1|a) by C1;
06: {} in On U implies g2.{} = U exp omega by A2;
07: for b st succ b in On U holds g2.succ b = C(b,g2.b) by B2;
08: for a st a in On U & a <> {} & a is limit_ordinal
    holds g2.a = D(a,g2|a) by C2;
    thus g1 = g2 from ORDINAL2:sch 4(01,02,03,04,05,06,07,08);
  end;
end;

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

theorem Unc1:
  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 EXCH1; then
      omega in On U by CLASSES2:10;
      hence omega in U by ORDINAL1:def 10;
    end;
    assume omega in U; then
    card omega in card U by CLASSES2:1;
    hence card U c/= omega;
  end;

theorem Th51:
  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
Z0: 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;
00: P[0];
01: for b st P[b] holds P[succ b]
    proof
      let b such that
Z1:   P[b] and
Z2:   succ b in U;
A0:   b in succ b by ORDINAL1:10;
      let a,c;
      assume a in succ b; then
A1:   a in b or a in {b} by XBOOLE_0:def 3;
      succ b in On U by Z2,ORDINAL1:def 10; then
A2:   F.succ b = criticals(F.b) by V;
      assume c in dom(F.succ b); then
A3:   F.(succ b).c is_a_fixpoint_of F.b by A2,Th02; 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 Z1,Z2,A0,A1,A3,TARSKI:def 1,ORDINAL1:19;
    end;
F1: dom F = On U by V;
02: 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
Z1:   b <> {} & b is limit_ordinal and
      for d st d in b holds P[d] and
Z3:   b in U;
B2:   b in On U by Z3,ORDINAL1:def 10; then
B0:   F.b = criticals(F|b) by Z1,V;
      b c= On U by B2,ORDINAL1:def 2; then
B3:   dom(F|b) = b by F1,RELAT_1:91;
      let a,c; assume
Z4:   a in b; then
B1:   F.a = (F|b).a by FUNCT_1:72;
      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 EXCH9;
      assume
      c in dom(F.b); then
      F.b.c in rng (F.b) by FUNCT_1:def 5; then
      F.b.c in X by B0,ThN1a; then
      consider z being Element of dom(g.0) such that
B4:   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 B3,B1,Z4,FUNCT_1:def 5;
      hence thesis by B4;
    end;
    for b holds P[b] from ORDINAL2:sch 1(00,01,02);
    hence thesis by Z0;
  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
Z0: l in U;
    assume
Z1: 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;
A0: 0 in l by ORDINAL3:10; then
    omega c= l by ORDINAL1:def 12; then
    reconsider o = omega as non trivial Ordinal of U by Z0,CLASSES1:def 1;
    F.0 = U exp o by V; then
    reconsider f0 = F.0 as normal Ordinal-Sequence of U;
A2: f0 = g.0 by ORDINAL3:10,FUNCT_1:72; then
A1: dom lims g = dom f0 & dom f0 = On U by LIM,FUNCT_2:def 1;
B3: a is_a_fixpoint_of f0 by Z1,ORDINAL3:10; then
A3: a in On U & a = f0.a by A1,ABIAN:def 3;
A5: dom F = On U by V;
    l in On U by Z0,ORDINAL1:def 10; then
    l c= dom F by A5,ORDINAL1:def 2; then
A6: dom g = l by RELAT_1:91;
    set lg = lims g;
    thus a in dom lims g by A1,B3,ABIAN:def 3;
A4: lg.a = u by A1,A3,LIM;
    {a} = X
    proof
      a in X by A0,A6,A3,A2;
      hence {a} c= X by ZFMISC_1:37;
      let x; assume x in X; then
      consider d being Element of dom g such that
A7:   x = g.d.a & d in dom g;
      g.d = F.d by A7,FUNCT_1:70; then
      a is_a_fixpoint_of g.d by Z1,A6; then
      x = a by A7,ABIAN:def 3;
      hence thesis by TARSKI:def 1;
    end;
    hence a = (lims g).a by A4,ZFMISC_1:31;
  end;

theorem Th52:
  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
A0: 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;
01: P[0];
02: for b st P[b] holds P[succ b]
    proof
      let b such that
A1:   P[b];
      let a,c such that
A2:   a c= succ b and
A3:   succ b in U and
A4:   c in dom(F.succ b);
      assume
Z0:   for c st c in succ b holds U-Veblen.c is normal;
      succ b in On U by A3,ORDINAL1:def 10; then
A5:   F.succ b = criticals (F.b) by V; then
A6:   dom(F.succ b) c= dom(F.b) by Th05;
Z1:   b in succ b by ORDINAL1:10; then
A7:   b in U by A3,ORDINAL1:19;
      F.b is normal by Z0,ORDINAL1:10; then
A8:   F.b.c c= F.succ b.c by A4,A5,Th40;
A9:   for c st c in b holds F.c is normal by Z0,Z1,ORDINAL1:19;
      per cases by A2,ORDINAL5:1;
      suppose a = succ b;
        hence thesis;
      end;
      suppose a c= b; then
        F.a.c c= F.b.c by A1,A4,A6,A7,A9;
        hence thesis by A8,XBOOLE_1:1;
      end;
    end;
03: for b st b <> {} & b is limit_ordinal & for d st d in b holds P[d]
    holds P[b]
    proof
      let b;
      assume
Z1:   b <> {} & b is limit_ordinal;
      assume for d st d in b holds P[d];
      let a,c;
      assume
Z3:   a c= b;
      per cases by Z3,XBOOLE_0:def 8;
      suppose a = b;
        hence thesis;
      end;
      suppose
C0:     a c< b; then
B0:     a in b by ORDINAL1:21;
        assume
        b in U; then
B1:     b in On U by ORDINAL1:def 10; then
B2:     F.b = criticals(F|b) by Z1,V;
        dom F = On U by V; then
        b c= dom F by B1,ORDINAL1:def 2; then
B4:     dom(F|b) = b by RELAT_1:91;
        assume
Z5:     c in dom(F.b);
       assume
Z7:     for c st c in b holds U-Veblen.c is normal;
Z6:     now let c; assume c in dom(F|b); then
          c in b & (F|b).c = F.c by B4,FUNCT_1:72;
          hence (F|b).c is normal by Z7;
        end;
B6:     (F|b).a in rng(F|b) by B0,B4,FUNCT_1:def 5;
        (F|b).a = F.a by C0,ORDINAL1:21,FUNCT_1:72;
        hence F.a.c c= F.b.c by B0,B2,B4,Z5,Z6,B6,ThAB;
      end;
    end;

    for b holds P[b] from ORDINAL2:sch 1(01,02,03);
    hence thesis by A0;
  end;

theorem Th53:
  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
Z0: l in U and
Z1: a in U and
Z2: b in l and
Z3: 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;
A0: 0 in l by ORDINAL3:10;
    reconsider f0 = F.0, f = F.b as normal Ordinal-Sequence of U
    by Z2,Z3,ORDINAL3:10;
A2: f0 = g.0 & f = g.b by Z2,ORDINAL3:10,FUNCT_1:72; then
A1: dom lims g = dom f0 by LIM .= On U by FUNCT_2:def 1;
A5: dom F = On U by V;
    l in On U by Z0,ORDINAL1:def 10; then
    l c= dom F by A5,ORDINAL1:def 2; then
A6: dom g = l by RELAT_1:91; then
A7: g.b.a in X by Z2;
    now
      let c; assume
C1:   c in dom g; then
      g.c = F.c by FUNCT_1:70;
      hence g.c is Ordinal-Sequence of U by A6,C1,Z3;
    end; then
    reconsider lg = lims g as Ordinal-Sequence of U by Z0,A6,ThL1;
A9: a in On U by Z1,ORDINAL1:def 10; then
A3: lg.a = u by A1,LIM;
A4: dom f = On U & dom f0 = On U by FUNCT_2:def 1;
A8: 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
B0:   x in X; then
      consider d being Element of dom g such that
B1:   x = g.d.a & d in dom g;
      reconsider f2 = F.d as normal Ordinal-Sequence of U by Z3,A6;
C2:   f2 = g.d by A6,FUNCT_1:72;
C3:   dom f2 = On U by FUNCT_2:def 1;
      omega c= l by A0,ORDINAL1:def 12; then
C4:   d in U & omega in U by A6,Z0,ORDINAL1:19,CLASSES1:def 1;
C5:   b in U by Z0,Z2,ORDINAL1:19;
C6:   for c st c in b holds U-Veblen.c is normal by Z3,Z2,ORDINAL1:19;
      per cases by ORDINAL1:26;
      suppose
        d c= b; then
B2:     x c= g.b.a by A9,A2,A4,B1,C2,C4,C5,C6,Th52;
        take y = g.(succ b).a;
B3:     b in succ b & succ b in l by Z2,ORDINAL1:10,41; then
        reconsider f1 = F.succ b as normal Ordinal-Sequence of U by Z3;
B4:     f1 = g.succ b by B3,FUNCT_1:72;
        succ b in U by B3,Z0,ORDINAL1:19; then
        succ b in On U by ORDINAL1:def 10; then
B6:     f1 = criticals f & dom f1 = On U by V,FUNCT_2:def 1; then
        f.a c= y by A9,B4,Th40;
        hence x c= y by B2,A2,XBOOLE_1:1;
        thus y in X by A6,B3;
        thus thesis by A9,B4,B6,Th02;
      end;
      suppose
C1:     b in d;
        take y = x;
        thus x c= y & y in X by B0;
        thus thesis by A9,B1,C1,C2,C3,C4,Th51;
      end;
    end;
    thus (lims(U-Veblen|l)).a in dom(U-Veblen.b) by A3,A4,ORDINAL1:def 10;
    hence thesis by A3,A7,A8,Th08a;
  end;

Th21:
  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 V;
    hence U-Veblen.0 is normal Ordinal-Sequence of U;
  end;

Th22:
  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
Z0: omega in U and
Z1: 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 Z1,CLASSES2:6;
    then succ a in On U by ORDINAL1:def 10;
    then U-Veblen.succ a = criticals f by V;
    hence U-Veblen.succ a is normal Ordinal-Sequence of U
    by Z0,Th39;
  end;

Th61:
  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
Z0: l in U;
    assume
Z1: for a st a in l holds U-Veblen.a is normal Ordinal-Sequence of U;
A0: l in On U by Z0,ORDINAL1:def 10; then
A1: U-Veblen.l = criticals(U-Veblen|l) by V;
A3: dom(U-Veblen) = On U by V;
    l c= On U by A0,ORDINAL1:def 2; then
A2: dom(U-Veblen|l) = l by A3,RELAT_1:91;
YY: dom (U-Veblen.l) = On U
    proof set F = U-Veblen; set G = F.l;
H1:   0 in l by ORDINAL3:10;
      reconsider f0 = F.0 as normal Ordinal-Sequence of U by Z1,ORDINAL3:10;
H2:   dom f0 = On U by FUNCT_2:def 1;
H2a:  f0 = (F|l).0 by ORDINAL3:10,FUNCT_1:72; then
      f0 in rng (F|l) by A2,H1,FUNCT_1:def 5;
      hence dom G c= On U by A1,H2,ThA5;
      now
        let c; assume
C1:     c in dom (F|l); then
        (F|l).c = F.c by FUNCT_1:70;
        hence (F|l).c is Ordinal-Sequence of U by A2,C1,Z1;
      end; then
      reconsider lg = lims (F|l) as Ordinal-Sequence of U by Z0,A2,ThL1;
H3:   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
G1:     x in dom lg & y = lg.x by FUNCT_1:def 5;
        reconsider x as Ordinal by G1;
G2:     x in U & y in On U by H3,G1,ORDINAL1:def 10;
        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};
G4:     Y is ordinal-membered by ThA1;
        now let f;
          assume f in rng(F|l); then
          consider z such that
G3:       z in l & f = (F|l).z by A2,FUNCT_1:def 5;
          f = F.z by G3,FUNCT_1:72;
          hence y is_a_fixpoint_of f by Z0,Z1,G3,G1,G2,Th53;
        end; then
        y in Y by H2,H2a,G2;
        hence thesis by A1,G4,ThN1a;
      end; then
F1:   Union lg c= Union G by ZFMISC_1:95;
      On U c= Union lg
      proof
        let a; assume
E1:     a in On U;
E2:     a in succ a by ORDINAL1:10;
        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:55; then
E3:     succ a in On U by E1,ORDINAL1:41; then
E4:     lg.succ a = union X by H3,LIM;
E5:     f0.succ a in X by H2a,A2,H1;
E6:     f0.a in f0.succ a by E2,E3,H2,ORDINAL2:def 16;
        a c= f0.a by H2,E1,ORDINAL4:10; then
        a in f0.succ a by E6,ORDINAL1:22; then
        a in lg.succ a by E4,E5,TARSKI:def 4;
        hence thesis by H3,E3,CARD_5:10;
      end; then
F2:   On U c= Union G by F1,XBOOLE_1:1;
F3:   rng G c= U
      proof let x;
        assume x in rng G; then
        consider y such that
D1:     y in dom G & x = G.y by FUNCT_1:def 5;
        x is_a_fixpoint_of f0 by A1,A2,H1,H2a,D1,ThA2; 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:26; then
      reconsider d = dom G as Ordinal of U by ORDINAL1:def 10;
H5:   card d in card U by CLASSES2:1;
      card rng G c= card d by CARD_1:28; then
      card rng G in card U by H5,ORDINAL1:22; then
      reconsider r = rng G as Element of U by F3,CLASSES1:2;
      union r in U; then
      Union G in On U by ORDINAL1:def 10; then
      Union G in Union G by F2;
      hence thesis;
    end;
ZZ: rng (U-Veblen.l) c= On U
    proof
      let x; assume x in rng(U-Veblen.l); then
      consider y such that
C1:   y in dom (U-Veblen.l) & x = (U-Veblen.l).y by FUNCT_1:def 5;
      reconsider y as Ordinal by C1;
C2:   0 in l by ORDINAL3:10; then
      x is_a_fixpoint_of (U-Veblen|l).0 by A1,C1,A2,ThA2; 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 Z1,C2,FUNCT_1:72;
      hence thesis by FUNCT_2:def 1;
    end;
    now let a;
      assume
B1:   a in l; then
      (U-Veblen|l).a = U-Veblen.a by FUNCT_1:72;
      hence (U-Veblen|l).a is normal by Z1,B1;
    end; then
    U-Veblen.l is continuous by A1,A2,ThAA;
    hence U-Veblen.l is normal Ordinal-Sequence of U by A1,YY,ZZ,FUNCT_2:4;
  end;

theorem Th23:
  omega in U & a in U implies U-Veblen.a is normal Ordinal-Sequence of U
  proof assume
Z0: omega in U;
    defpred P[Ordinal] means
    $1 in U implies U-Veblen.$1 is normal Ordinal-Sequence of U;
00: P[0] by Z0,Th21;
01: P[b] implies P[succ b]
    proof
      b in succ b by ORDINAL1:10;
      then succ b in U implies b in U by ORDINAL1:19;
      hence thesis by Z0,Th22;
    end;
02: b <> {} & b is limit_ordinal & (for c st c in b holds P[c]) implies P[b]
    proof assume that
A1:   b <> {} & b is limit_ordinal and
A2:   for c st c in b holds P[c] and
A3:   b in U;
      now
        let a; assume
A4:     a in b;
        then a in U by A3,ORDINAL1:19;
        hence U-Veblen.a is normal Ordinal-Sequence of U by A2,A4;
      end;
      hence thesis by A1,A3,Th61;
    end;
    P[b] from ORDINAL2:sch 1(00,01,02);
    hence thesis;
  end;

theorem Th24:
  omega in U & U c= W & a in U implies U-Veblen.a c= W-Veblen.a
  proof assume
A0: omega in U & U c= W; then
B0: On U c= On W by ORDINAL2:11;
    defpred P[ordinal number] means
    $1 in U implies U-Veblen.$1 c= W-Veblen.$1;
A1: U-Veblen.0 = U exp omega & W-Veblen.0 = W exp omega by V;
A2: 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 10;
      a in U; then
      reconsider b = a as Ordinal of W by A0;
      (U exp omega).a = exp(omega,b) by A0,EXP;
      hence (U exp omega).x = (W exp omega).x by A0,EXP;
    end; then
00: P[0] by B0,A1,A2,GRFUNC_1:8;
01: P[b] implies P[succ b]
    proof assume
S2:   P[b]; assume
S4:   succ b in U;
S5:   b in succ b by ORDINAL1:10;
      succ b in On U & succ b in On W by A0,S4,ORDINAL1:def 10; then
      U-Veblen.succ b = criticals (U-Veblen.b) &
      W-Veblen.succ b = criticals (W-Veblen.b) by V;
      hence thesis by S2,S5,Th0A,S4,ORDINAL1:19;
    end;
02: b <> {} & b is limit_ordinal & (for c st c in b holds P[c]) implies P[b]
    proof assume that
A1:   b <> {} & b is limit_ordinal and
A2:   for c st c in b holds P[c] and
A3:   b in U;
      set g1 = U-Veblen|b, g2 = W-Veblen|b;
A5:   b in On U & b in On W by A0,A3,ORDINAL1:def 10; then
A4:   U-Veblen.b = criticals g1 & W-Veblen.b = criticals g2 by A1,V;
      dom(U-Veblen) = On U & dom(W-Veblen) = On W by V; then
      b c= dom(U-Veblen) & b c= dom(W-Veblen) by A5,ORDINAL1:def 2; then
A6:   dom g1 = b & dom g2 = b by RELAT_1:91;
      now
        let a; assume
A7:     a in dom g1; then
A8:     g1.a = U-Veblen.a & g2.a = W-Veblen.a by A6,FUNCT_1:70;
        a in U by A3,A6,A7,ORDINAL1:19;
        hence g1.a c= g2.a by A2,A6,A7,A8;
      end;
      hence thesis by A1,A4,A6,ThAC;
    end;
    P[b] from ORDINAL2:sch 1(00,01,02);
    hence thesis;
  end;

theorem Th25:
  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
A0: omega in U & a in U & b in U & omega in W & a in W & b in W; then
A1: a in On U & a in On W by ORDINAL1:def 10;
    W-Veblen.b is Ordinal-Sequence of W &
    U-Veblen.b is Ordinal-Sequence of U by A0,Th23; then
A2: 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:57; 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 A0,Th24;
    hence thesis by A1,A2,GRFUNC_1:8;
  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:10; then
    omega c= l by ORDINAL1:def 12; then
A3: omega in U & l in On U by A1,ORDINAL1:def 10,CLASSES1:def 1; then
A4: G.l = criticals(G|l) & dom G = On U by V;
    l c= On U by A3,ORDINAL1:def 2; then
A5: dom(G|l) = l by A4,RELAT_1:91;
    set g = G|l;
    now let a; assume
A6:   a in dom g; then
      g.a = G.a by A5,FUNCT_1:72;
      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,ThL1;
    g.0 = G.0 by FUNCT_1:72,ORDINAL3:10; then
    reconsider g0 = g.0 as Ordinal-Sequence of U by A2,ORDINAL3:10;
A8: 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};
A7: f is non-decreasing
    proof
      let a,b; assume
B1:   a in b & b in dom f; then
      a in dom f by ORDINAL1:19; then
B3:   f.a = union X(a) & f.b = union X(b) by B1,LIM;
      let c; assume c in f.a; then
      consider x such that
B4:   c in x & x in X(a) by B3,TARSKI:def 4;
      consider xa being Element of dom g such that
B5:   x = g.xa.a & xa in dom g by B4;
      g.xa = G.xa by A5,FUNCT_1:72; 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 A8,B1,ORDINAL2:def 16; then
      h.a c= h.b by ORDINAL1:def 2; then
      c in h.b & h.b in X(b) by B4,B5;
      hence c in f.b by B3,TARSKI:def 4;
    end;
    f is continuous
    proof let a,b; assume
C1:   a in dom f & a <> {} & a is limit_ordinal & b = f.a; then
C2:   b = union X(a) by LIM;
D1:   a c= dom f by C1,ORDINAL1:def 2; then
C3:   dom(f|a) = a by RELAT_1:91;
C4:   b = Union(f|a)
      proof
        thus b c= Union(f|a)
        proof
          let c; assume c in b; then
          consider x such that
B4:       c in x & x in X(a) by C2,TARSKI:def 4;
          consider xa being Element of dom g such that
B5:       x = g.xa.a & xa in dom g by B4;
          g.xa = G.xa by A5,FUNCT_1:72; then
          reconsider h = g.xa as normal Ordinal-Sequence of U
          by A2,A5;
C6:       dom h = On U by FUNCT_2:def 1; then
C5:       h.a is_limes_of h|a by A8,C1,ORDINAL2:def 17;
C7:       h|a is increasing by ORDINAL4:15;
C8:       dom(h|a) = a by A8,D1,C6,RELAT_1:91; then
          Union(h|a) is_limes_of h|a by C1,C7,ORDINAL5:6; then
          lim(h|a) = Union(h|a) by ORDINAL2:def 14; then
          h.a = Union(h|a) by C5,ORDINAL2:def 14; then
          consider y such that
C9:       y in a & c in (h|a).y by B4,B5,C8,CARD_5:10;
D3:       y in On U by A8,C1,C9,ORDINAL1:19;
          (h|a).y = h.y by C9,FUNCT_1:72; then
          (h|a).y in X(y) by B5; then
          c in union X(y) by C9,TARSKI:def 4; then
          c in f.y by A8,D3,LIM; then
          c in (f|a).y by C9,FUNCT_1:72;
          hence thesis by C3,C9,CARD_5:10;
        end;
        let c; assume c in Union(f|a); then
        consider x such that
E1:     x in dom(f|a) & c in (f|a).x by CARD_5:10;
E2:     (f|a).x = f.x by C3,E1,FUNCT_1:72;
        x in dom f by E1,RELAT_1:86; then
        f.x = union X(x) by LIM; then
        consider y such that
E4:     c in y & y in X(x) by E1,E2,TARSKI:def 4;
        consider z being Element of dom g such that
E5:     y = g.z.x & z in dom g by E4;
        g.z = G.z by A5,FUNCT_1:72; 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 E1,C3,C1,A8,ORDINAL2:def 16; then
        h.x c= h.a by ORDINAL1:def 2; then
        c in h.a & h.a in X(a) by E4,E5;
        hence c in b by C2,TARSKI:def 4;
      end;
      f|a is non-decreasing by A7,ThND;
      hence b is_limes_of f|a by C1,C3,C4,ORDINAL5:6;
    end;
    hence thesis by A7;
  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 XBOOLE_1:7,CLASSES1:5; then
    omega in U by CLASSES1:def 1;
    hence thesis by Unc1;
  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 LemT:
  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 XBOOLE_1:1,CLASSES1:5;
    hence thesis by CLASSES1:def 1;
  end;

theorem Th26:
  omega in U & a in U & b in U implies b-Veblen a = U-Veblen.b.a
  proof assume
Z0: 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 Unc1,LemT;
    hence b-Veblen a = U-Veblen.b.a by Z0,Th25;
  end;

theorem Th10:
  0-Veblen(a) = exp(omega,a)
  proof
    set b = 0\/a\/omega;
    set U = Tarski-Class b;
    b in U by CLASSES1:5; then
00: b in On U by ORDINAL1:def 10;
    omega in On U by 00,XBOOLE_1:7,ORDINAL1:22; then
A0: omega in U by ORDINAL1:def 10;
    a in On U by 00,XBOOLE_1:7,ORDINAL1:22; then
A1: a in U by ORDINAL1:def 10;
    thus 0-Veblen(a) = (U exp omega).a by V
    .= exp(omega,a) by A1,A0,EXP;
  end;

theorem Th11:
  b-Veblen((succ b)-Veblen a) = (succ b)-Veblen a
  proof set U = Tarski-Class(b\/a\/omega);
A2: omega in U by Unc1;
    reconsider b1 = b as Ordinal of U by LemT;
    succ b1 in On U by ORDINAL1:def 10; then
A4: U-Veblen.(succ b) = criticals (U-Veblen.b) by V;
    reconsider f = U-Veblen.b1, g = U-Veblen.(succ b1) as
    normal Ordinal-Sequence of U by A2,Th23;
A1: a in U by LemT; then
A3: a in On U by ORDINAL1:def 10;
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 Unc1;
    then
A7: (succ b1)-Veblen a = g.a & b1-Veblen(g.a) = f.(g.a) by A1,Th26; then
    (succ b)-Veblen a is_a_fixpoint_of U-Veblen.b by A3,A4,A5,Th02;
    hence b-Veblen((succ b)-Veblen a) = (succ b)-Veblen a by A7,ABIAN:def 3;
  end;

theorem Th11a:
  b in c implies b-Veblen(c-Veblen a) = c-Veblen a
  proof assume
Z0: b in c;
    set U = Tarski-Class(c\/a\/omega);
A0: omega in U by Unc1;
A1: a in U & c in U by LemT; then
A2: b in U by Z0,ORDINAL1:19; then
    reconsider f = U-Veblen.b, g = U-Veblen.c as normal Ordinal-Sequence of U
    by A0,LemT,Th23;
    dom g = On U by FUNCT_2:def 1; then
    a in dom g by A1,ORDINAL1:def 10; then
    g.a is_a_fixpoint_of f by Z0,A0,LemT,Th51; then
    g.a = f.(g.a) by ABIAN:def 3;
    hence b-Veblen(c-Veblen a) = c-Veblen a by A0,A2,Th26;
  end;

theorem Th15:
  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);
A0: n in omega & omega in U & omega in W by Unc1,ORDINAL1:def 13;
A1: b in U & c in U by LemT;
A2: a in W & c in W by LemT;
    reconsider f = U-Veblen.c as increasing Ordinal-Sequence of U
    by A0,LemT,Th23;
    reconsider g = W-Veblen.c as increasing Ordinal-Sequence of W
    by A0,LemT,Th23;
A3: dom f = On U & dom g = On W by FUNCT_2:def 1;
A4: b in On U & a in On W by A1,A2,ORDINAL1:def 10;
    hereby
      assume
B1:   a c= b; then
B2:   a in U by A1,CLASSES1:def 1;
      per cases by B1,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:21; then
        f.a in f.b by A3,A4,ORDINAL2:def 16; then
        c-Veblen a in c-Veblen b by B2,A0,A1,A2,Th25;
        hence c-Veblen a c= c-Veblen b by ORDINAL1:def 2;
      end;
    end;
    assume
A5: c-Veblen a c= c-Veblen b & a c/= b; then
A6: b in a by ORDINAL1:26; then
A7: b in W by A2,ORDINAL1:19;
    g.b in g.a by A3,A4,A6,ORDINAL2:def 16; then
    c-Veblen b in c-Veblen a by A0,A1,A2,A7,Th25; then
    c-Veblen b in c-Veblen b by A5;
    hence thesis;
  end;

theorem Th15a:
  a in b iff c-Veblen a in c-Veblen b
  proof
    b c= a iff c-Veblen b c= c-Veblen a by Th15;
    hence thesis by EXCH1;
  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
Z0:     a-Veblen b in c-Veblen d;
        per cases by ORDINAL1:24;
        case a = c;
          hence b in d by Z0,Th15a;
        end;
        case a in c; then
          a-Veblen(c-Veblen d) = c-Veblen d by Th11a;
          hence b in c-Veblen d by Z0,Th15a;
        end;
        case c in a; then
          c-Veblen(a-Veblen b) = a-Veblen b by Th11a;
          hence a-Veblen b in d by Z0,Th15a;
        end;
      end;
      assume
Z3:   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 Z3;
      suppose a = c & b in d;
        hence a-Veblen b in c-Veblen d by Th15a;
      end;
      suppose
Z4:     a in c & b in c-Veblen d; then
        a-Veblen(c-Veblen d) = c-Veblen d by Th11a;
        hence a-Veblen b in c-Veblen d by Z4,Th15a;
      end;
      suppose
Z5:     c in a & a-Veblen b in d; then
        c-Veblen(a-Veblen b) = a-Veblen b by Th11a;
        hence a-Veblen b in c-Veblen d by Z5,Th15a;
      end;
    end;

begin :: Epsilon Numbers

reserve U for uncountable Universe;

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

theorem Th13:
  1-Veblen(a) is epsilon
  proof set U = Tarski-Class(a\/omega);
    0-Veblen(1-Veblen a) = (succ 0)-Veblen a by Th11;
    hence exp(omega,1-Veblen a) = 1-Veblen a by Th10;
  end;

theorem Th14:
  for e being epsilon Ordinal ex a st e = 1-Veblen a
  proof
    let e be epsilon Ordinal;
    set U = Tarski-Class(e\/omega);
A0: omega in U by Unc1;
    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 A0,Th23;
A1: g = criticals(U exp omega) by Th12
    .= criticals f by V;
A2: f.e = 0-Veblen e .= exp(omega,e) by Th10 .= e by ORDINAL5:def 5;
A3: dom f = On U by FUNCT_2:def 1;
    e c= e\/omega & e\/omega in U by XBOOLE_1:7,CLASSES1:5; then
A5: e in U by CLASSES1:def 1; then
    e in On U by ORDINAL1:def 10; then
    e is_a_fixpoint_of f by A2,A3,ABIAN:def 3; then
    consider a such that
A4: a in dom criticals f & e = (criticals f).a by Th06;
    take a;
    set W = Tarski-Class(a\/omega);
A6: a c= a\/omega & a\/omega in W by XBOOLE_1:7,CLASSES1:5;
    a c= e by A4,ORDINAL4:10; then
    omega in W & a in W & a in U & 1-element_of U = 1-element_of W
    by A5,A6,Unc1,CLASSES1:def 1;
    hence e = 1-Veblen a by A0,A1,A4,Th25;
  end;

Th16:
  1-Veblen 0 = epsilon_0
  proof
    consider b such that
A0: 1-Veblen 0 = epsilon_b by Th13,ORDINAL5:51;
    consider a such that
A1: epsilon_0 = 1-Veblen a by Th14;
    now assume b <> 0; then
      epsilon_0 in epsilon_b by ORDINAL3:10,ORDINAL5:44;
      hence contradiction by A0,A1,Th15a;
    end;
    hence thesis by A0;
  end;

Th17:
  1-Veblen a = epsilon_a implies 1-Veblen succ a = epsilon_succ a
  proof
    assume
Z0: 1-Veblen a = epsilon_a;
    consider b such that
A0: 1-Veblen succ a = epsilon_b by Th13,ORDINAL5:51;
    consider c such that
A1: epsilon_succ a = 1-Veblen c by Th14;
A2: a in succ a by ORDINAL1:10;
    epsilon_a in epsilon_succ a by ORDINAL1:10,ORDINAL5:44; then
    a in c by Z0,A1,Th15a; then
    succ a c= c by ORDINAL1:33;
    hence 1-Veblen succ a c= epsilon_succ a by A1,Th15;
    assume epsilon_succ a c/= 1-Veblen succ a; then
    epsilon_b in epsilon_succ a by A0,EXCH1; then
    b in succ a by LemE2; then
    b c= a by ORDINAL1:34; then
    epsilon_b c= epsilon_a by LemE1; then
    succ a c= a by Z0,A0,Th15; then
    a in a by A2;
    hence thesis;
  end;

Th18:
  (for a st a in l holds 1-Veblen(a) = epsilon_a)
  implies 1-Veblen(l) = epsilon_l
  proof assume
Z0: for a st a in l holds 1-Veblen(a) = epsilon_a;
    set U = Tarski-Class(l\/omega);
    0 in l by ORDINAL3:10; then
    omega c= l by ORDINAL1:def 12; then
    l\/omega = l by XBOOLE_1:12; then
A1: l in U by CLASSES1:5;
A2: omega in U by Unc1;
    1-element_of U = 1; then
    reconsider g = U-Veblen.1 as normal Ordinal-Sequence of U
    by A2,Th23;
    reconsider o = omega as non trivial Ordinal of U by Unc1;
    set f = U exp o;
A4: g = criticals f by Th12;
B0: dom g = On U by FUNCT_2:def 1; then
B1: l in dom g by A1,ORDINAL1:def 10; then
A5: g.l = Union(g|l) by A4,Th09 .= union rng(g|l);
    l c= dom g by B1,ORDINAL1:def 2; then
B2: dom(g|l) = l by RELAT_1:91;
    now let x;
      assume x in rng(g|l); then
      consider y such that
A6:   y in dom(g|l) & x = (g|l).y by FUNCT_1:def 5;
      reconsider y as Ordinal by A6;
A7:   x = g.y by A6,FUNCT_1:70;
      y in dom g by B1,B2,A6,ORDINAL1:19; then
      y in U & 1-element_of U in U by B0,ORDINAL1:def 10; then
      x = 1-Veblen y by A2,A7,Th26; then
      x = epsilon_y by Z0,B2,A6; then
      x in epsilon_l by B2,A6,LemE2;
      hence x c= epsilon_l by ORDINAL1:def 2;
    end;
    hence 1-Veblen(l) c= epsilon_l by A5,ZFMISC_1:94;
    let a; assume a in epsilon_l; then
    consider b such that
A8: b in l & a in epsilon_b by ORDINAL5:47;
    epsilon_b = 1-Veblen b by Z0,A8; then
    epsilon_b in 1-Veblen l by A8,Th15a;
    hence thesis by A8,ORDINAL1:19;
  end;

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