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

environ

 vocabularies ORDINAL1, FUNCT_1, XBOOLE_0, TARSKI, ZFMISC_1, RELAT_1, SETFAM_1,
      SUBSET_1, FUNCOP_1, ORDINAL2, NAT_1, CARD_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
      SETFAM_1, FUNCOP_1;
 constructors SETFAM_1, ORDINAL1, FUNCOP_1;
 registrations SUBSET_1, FUNCT_1, ORDINAL1, FUNCOP_1;
 requirements SUBSET, BOOLE, NUMERALS;
 definitions ORDINAL1, TARSKI, XBOOLE_0;
 equalities ORDINAL1, XBOOLE_0;
 expansions ORDINAL1, TARSKI, XBOOLE_0;
 theorems TARSKI, ORDINAL1, SETFAM_1, ZFMISC_1, FUNCT_1, RELAT_1, XBOOLE_1,
      FUNCOP_1, XTUPLE_0;
 schemes XBOOLE_0, FUNCT_1, ORDINAL1;

begin

reserve A,A1,A2,B,C,D for Ordinal,
  X,Y for set,
  x,y,a,b,c for object,
  L,L1,L2,L3 for Sequence,
  f for Function;

scheme
  OrdinalInd { P[Ordinal] } : for A holds P[A]
provided
A1: P[0] and
A2: for A st P[A] holds P[succ A] and
A3: for A st A <> 0 & A is limit_ordinal & for B st B in A holds P[B]
holds P[A]
proof
A4: for A st for B st B in A holds P[B] holds P[A]
  proof
    let A such that
A5: for B st B in A holds P[B];
A6: A <> 0 & (for B holds A <> succ B) implies thesis by A3,A5,ORDINAL1:29;
    now
      given B such that
A7:   A = succ B;
      B in A by A7,ORDINAL1:6;
      hence thesis by A2,A5,A7;
    end;
    hence thesis by A1,A6;
  end;
  thus for A holds P[A] from ORDINAL1:sch 2(A4);
end;

theorem Th1:
  A c= B iff succ A c= succ B
proof
  A c= B iff A in succ B by ORDINAL1:22;
  hence thesis by ORDINAL1:21;
end;

theorem Th2:
  union succ A = A
proof
  thus union succ A c= A
  proof
    let x be object;
    assume x in union succ A;
    then consider X such that
A1: x in X and
A2: X in succ A by TARSKI:def 4;
    reconsider X as Ordinal by A2;
    X c= A by A2,ORDINAL1:22;
    hence thesis by A1;
  end;
  thus thesis by ORDINAL1:6,ZFMISC_1:74;
end;

theorem
  succ A c= bool A
proof
  let x be object;
  assume
A1: x in succ A;
  then reconsider B = x as Ordinal;
  x in A or x = A by A1,ORDINAL1:8;
  then B c= A by ORDINAL1:def 2;
  hence thesis;
end;

theorem
  0 is limit_ordinal
by ZFMISC_1:2;

theorem Th5:
  union A c= A
proof
  let x be object;
  assume x in union A;
  then consider Y such that
A1: x in Y and
A2: Y in A by TARSKI:def 4;
  Y c= A by A2,ORDINAL1:def 2;
  hence thesis by A1;
end;

definition
  let L;
  func last L -> set equals
  L.(union dom L);
  coherence;
end;

theorem
  dom L = succ A implies last L = L.A by Th2;

theorem
  On X c= X
by ORDINAL1:def 9;

theorem Th8:
  On A = A
proof
  for x being object holds x in A iff x in A & x is Ordinal;
  hence thesis by ORDINAL1:def 9;
end;

theorem Th9:
  X c= Y implies On X c= On Y
proof
  assume
A1: X c= Y;
  let x be object;
  assume x in On X;
  then x in X & x is Ordinal by ORDINAL1:def 9;
  hence thesis by A1,ORDINAL1:def 9;
end;

theorem
  Lim X c= X
by ORDINAL1:def 10;

theorem
  X c= Y implies Lim X c= Lim Y
proof
  assume
A1: X c= Y;
  let x be object;
  assume x in Lim X;
  then x in X & ex A st x = A & A is limit_ordinal by ORDINAL1:def 10;
  hence thesis by A1,ORDINAL1:def 10;
end;

theorem
  Lim X c= On X
proof
  let x be object;
  assume x in Lim X;
  then x in X & ex A st x = A & A is limit_ordinal by ORDINAL1:def 10;
  hence thesis by ORDINAL1:def 9;
end;

theorem Th13:
  (for x st x in X holds x is Ordinal) implies meet X is Ordinal
proof
  assume
A1: for x st x in X holds x is Ordinal;
  now
    defpred P[Ordinal] means $1 in X;
    set x = the Element of X;
    assume
A2: X <> 0;
    then x is Ordinal by A1;
    then
A3: ex A st P[A] by A2;
    consider A such that
A4: P[A] & for B st P[B] holds A c= B from ORDINAL1:sch 1(A3);
    for x being object holds x in A iff for Y st Y in X holds x in Y
    proof
      let x be object;
      thus x in A implies for Y st Y in X holds x in Y
      proof
        assume
A5:     x in A;
        let Y;
        assume
A6:     Y in X;
        then reconsider B = Y as Ordinal by A1;
        A c= B by A4,A6;
        hence thesis by A5;
      end;
      assume for Y st Y in X holds x in Y;
      hence thesis by A4;
    end;
    hence thesis by A2,SETFAM_1:def 1;
  end;
  hence thesis by SETFAM_1:def 1;
end;

registration
  cluster limit_ordinal for Ordinal;
  existence
  proof
    take omega;
    thus thesis by ORDINAL1:def 11;
  end;
end;

definition
  let X;

  func inf X -> Ordinal equals
  meet On X;
  coherence
  proof
    x in On X implies x is Ordinal by ORDINAL1:def 9;
    hence thesis by Th13;
  end;
  func sup X -> Ordinal means
  :Def3:
  On X c= it & for A st On X c= A holds it c= A;
  existence
  proof
    defpred P[Ordinal] means On X c= $1;
    x in On X implies x is Ordinal by ORDINAL1:def 9;
    then reconsider A = union On X as epsilon-transitive epsilon-connected set
      by ORDINAL1:23;
    On X c= succ A
    proof
      let x be object;
      assume
A1:   x in On X;
      then reconsider B = x as Ordinal by ORDINAL1:def 9;
      B c= A by A1,ZFMISC_1:74;
      hence thesis by ORDINAL1:22;
    end;
    then
A2: ex A st P[A];
    thus ex F being Ordinal st P[F] & for A st P[A] holds F c= A from ORDINAL1
    :sch 1(A2);
  end;
  uniqueness;
end;

theorem
  A in X implies inf X c= A
proof
  assume A in X;
  then A in On X by ORDINAL1:def 9;
  hence thesis by SETFAM_1:3;
end;

theorem
  On X <> 0 & (for A st A in X holds D c= A) implies D c= inf X
proof
  assume that
A1: On X <> 0 and
A2: for A st A in X holds D c= A;
  let x be object such that
A3: x in D;
  for Y st Y in On X holds x in Y
  proof
    let Y;
    assume
A4: Y in On X;
    then reconsider A = Y as Ordinal by ORDINAL1:def 9;
    A in X by A4,ORDINAL1:def 9;
    then D c= A by A2;
    hence thesis by A3;
  end;
  hence thesis by A1,SETFAM_1:def 1;
end;

theorem
  A in X & X c= Y implies inf Y c= inf X
proof
  assume A in X;
  then
A1: On X <> 0 by ORDINAL1:def 9;
  assume X c= Y;
  then On X c= On Y by Th9;
  hence thesis by A1,SETFAM_1:6;
end;

theorem
  A in X implies inf X in X
proof
  defpred P[Ordinal] means $1 in X;
  assume A in X;
  then
A1: ex A st P[A];
  consider A such that
A2: P[A] & for B st P[B] holds A c= B from ORDINAL1:sch 1(A1);
A3: A in On X by A2,ORDINAL1:def 9;
A4: now
    let x be object;
    thus x in A implies for Y st Y in On X holds x in Y
    proof
      assume
A5:   x in A;
      let Y;
      assume
A6:   Y in On X;
      then reconsider B = Y as Ordinal by ORDINAL1:def 9;
      Y in X by A6,ORDINAL1:def 9;
      then A c= B by A2;
      hence thesis by A5;
    end;
    assume for Y st Y in On X holds x in Y;
    hence x in A by A3;
  end;
  On X <> 0 by A2,ORDINAL1:def 9;
  hence thesis by A2,A4,SETFAM_1:def 1;
end;

theorem Th18:
  sup A = A
proof
  On A = A & for B st On A c= B holds A c= B by Th8;
  hence thesis by Def3;
end;

theorem Th19:
  A in X implies A in sup X
proof
  assume A in X;
  then
A1: A in On X by ORDINAL1:def 9;
  On X c= sup X by Def3;
  hence thesis by A1;
end;

theorem Th20:
  (for A st A in X holds A in D) implies sup X c= D
proof
  assume
A1: for A st A in X holds A in D;
  On X c= D
  proof
    let x be object;
    assume
A2: x in On X;
    then reconsider A = x as Ordinal by ORDINAL1:def 9;
    A in X by A2,ORDINAL1:def 9;
    hence thesis by A1;
  end;
  hence thesis by Def3;
end;

theorem
  A in sup X implies ex B st B in X & A c= B
proof
  assume that
A1: A in sup X and
A2: for B st B in X holds not A c= B;
  for B st B in X holds B in A by A2,ORDINAL1:16;
  then sup X c= A by Th20;
  hence contradiction by A1,ORDINAL1:5;
end;

theorem
  X c= Y implies sup X c= sup Y
proof
  assume X c= Y;
  then
A1: On X c= On Y by Th9;
  On Y c= sup Y by Def3;
  then On X c= sup Y by A1;
  hence thesis by Def3;
end;

theorem
  sup { A } = succ A
proof
A1: On { A } c= succ A
  proof
    let x be object;
    assume x in On { A };
    then x in { A } by ORDINAL1:def 9;
    then x = A by TARSKI:def 1;
    hence thesis by ORDINAL1:6;
  end;
  now
    A in { A } by TARSKI:def 1;
    then
A2: A in On { A } by ORDINAL1:def 9;
    let B;
    assume On { A } c= B;
    hence succ A c= B by A2,ORDINAL1:21;
  end;
  hence thesis by A1,Def3;
end;

theorem
  inf X c= sup X
proof
  let x be object;
  set y = the Element of On X;
  assume
A1: x in inf X;
  then reconsider y as Ordinal by ORDINAL1:def 9,SETFAM_1:1;
  On X c= sup X by Def3;
  then y in sup X by A1,SETFAM_1:1;
  then
A2: y c= sup X by ORDINAL1:def 2;
  x in y by A1,SETFAM_1:1,def 1;
  hence thesis by A2;
end;

scheme
  TSLambda { A()->Ordinal, F(Ordinal)->set } : ex L st dom L = A() & for A st
  A in A() holds L.A = F(A) proof
  deffunc G(object) = F(sup union { $1 });
  consider f such that
A1: dom f = A() & for x being object st x in A() holds f.x = G(x)
from FUNCT_1:sch 3;
  reconsider f as Sequence by A1,ORDINAL1:def 7;
  take L = f;
  thus dom L = A() by A1;
  let A;
  assume A in A();
  hence L.A = F(sup union { A }) by A1
    .= F(sup A) by ZFMISC_1:25
    .= F(A) by Th18;
end;

definition
  let f;
  attr f is Ordinal-yielding means
  :Def4:
  ex A st rng f c= A;
end;

registration
  cluster Ordinal-yielding for Sequence;
  existence
  proof
    set A = the Ordinal;
    set L = the Sequence of A;
    take L,A;
    thus thesis by RELAT_1:def 19;
  end;
end;

definition
  mode Ordinal-Sequence is Ordinal-yielding Sequence;
end;

registration
  let A;
  cluster -> Ordinal-yielding for Sequence of A;
  coherence
  by RELAT_1:def 19;
end;

registration
  let L be Ordinal-Sequence;
  let A;
  cluster L|A -> Ordinal-yielding;
  coherence
  proof
    consider B such that
A1: rng L c= B by Def4;
    L|A is Ordinal-yielding
    proof
      take B;
      rng(L|A) c= rng L by RELAT_1:70;
      hence thesis by A1;
    end;
    hence thesis;
  end;
end;

reserve fi,psi for Ordinal-Sequence;

theorem Th25:
  A in dom fi implies fi.A is Ordinal
proof
  assume A in dom fi;
  then
A1: fi.A in rng fi by FUNCT_1:def 3;
  ex B st rng fi c= B by Def4;
  hence thesis by A1;
end;

registration
  let f be Ordinal-Sequence, a be object;
  cluster f.a -> ordinal;
  coherence
  proof
    a in dom f or not a in dom f;
    hence thesis by Th25,FUNCT_1:def 2;
  end;
end;

scheme
  OSLambda { A()->Ordinal, F(Ordinal)->Ordinal } : ex fi st dom fi = A() & for
  A st A in A() holds fi.A = F(A) proof
  consider L such that
A1: dom L = A() & for A st A in A() holds L.A = F(A) from TSLambda;
  L is Ordinal-yielding
  proof
    take sup rng L;
    let x be object;
    assume
A2: x in rng L;
    then consider y being object such that
A3: y in dom L and
A4: x = L.y by FUNCT_1:def 3;
    reconsider y as Ordinal by A3;
    L.y = F(y) by A1,A3;
    then
A5: x in On rng L by A2,A4,ORDINAL1:def 9;
    On rng L c= sup rng L by Def3;
    hence thesis by A5;
  end;
  then reconsider L as Ordinal-Sequence;
  take fi = L;
  thus dom fi = A() by A1;
  let A;
  assume A in A();
  hence thesis by A1;
end;

scheme
  TSUniq1 { A()->Ordinal, B()->object, C(Ordinal,set)->object,
   D(Ordinal,Sequence)->object, L1()->Sequence, L2()->Sequence } :
  L1() = L2()
provided
A1: dom L1() = A() and
A2: 0 in A() implies L1().0 = B() and
A3: for A st succ A in A() holds L1().(succ A) = C(A,L1().A) and
A4: for A st A in A() & A <> 0 & A is limit_ordinal holds L1().A = D(A,
L1()|A) and
A5: dom L2() = A() and
A6: 0 in A() implies L2().0 = B() and
A7: for A st succ A in A() holds L2().(succ A) = C(A,L2().A) and
A8: for A st A in A() & A <> 0 & A is limit_ordinal holds L2().A = D(A,
L2()|A)
proof
  defpred P[object] means L1().$1 <> L2().$1;
  consider X such that
A9: for Y being object holds Y in X iff Y in A() & P[Y] from XBOOLE_0:sch 1;
  for b being object holds b in X implies b in A() by A9;
  then
A10: X c= A();
  assume L1() <> L2();
  then ex a being object st a in A() & L1().a <> L2().a by A1,A5,FUNCT_1:2;
  then X <> 0 by A9;
  then consider B such that
A11: B in X and
A12: for C st C in X holds B c= C by A10,ORDINAL1:20;
A13: B in A() by A9,A11;
  then
A14: B c= A() by ORDINAL1:def 2;
  then
A15: dom(L1()|B) = B & dom(L2()|B) = B by A1,A5,RELAT_1:62;
A16: now
    let C;
    assume
A17: C in B;
    then not C in X by A12,ORDINAL1:5;
    hence L1().C = L2().C by A9,A14,A17;
  end;
A18: now
    let a be object;
    assume
A19: a in B;
    L1()|B.a = L1().a & L2()|B.a = L2().a by A15,A19,FUNCT_1:47;
    hence L1()|B.a = L2()|B.a by A16,A19;
  end;
A20: now
    given C such that
A21: B = succ C;
A22: L1().C = L1()|B.C & L2().C = L2()|B.C by A21,FUNCT_1:49,ORDINAL1:6;
    L1().B = C(C,L1().C) & L2().B = C(C,L2().C) by A3,A7,A13,A21;
    hence L1().B = L2().B by A18,A21,A22,ORDINAL1:6;
  end;
  now
    assume that
A23: B <> 0 and
A24: for C holds B <> succ C;
    B is limit_ordinal by A24,ORDINAL1:29;
    then L1().B = D(B,L1()|B) & L2().B = D(B,L2()|B) by A4,A8,A13,A23;
    hence L1().B = L2().B by A15,A18,FUNCT_1:2;
  end;
  hence contradiction by A2,A6,A9,A11,A20;
end;

scheme
  TSExist1 { A()->Ordinal, B()->object, C(Ordinal,set)->object,
     D(Ordinal,Sequence)->object } :
  ex L st dom L = A() & (0 in A() implies L.0 = B() ) & (for A st
  succ A in A() holds L.(succ A) = C(A,L.A) ) & for A st A in A() & A <> 0 & A
  is limit_ordinal holds L.A = D(A,L|A);
  defpred P[Ordinal,Sequence] means dom $2 = $1 & (0 in $1 implies $2.0 =
B() ) & (for A st succ A in $1 holds $2.(succ A) = C(A,$2.A) ) & for A st A in
  $1 & A <> 0 & A is limit_ordinal holds $2.A = D(A,$2|A);
  defpred R[Ordinal] means ex L st P[$1,L];
A1: for B st for C st C in B holds R[C] holds R[B]
  proof
    defpred R[object,object] means
    $1 is Ordinal & $2 is Sequence & for A,L st A = $1 & L = $2 holds P[A,L];
    let B such that
A2: for C st C in B ex L st P[C,L];
A3: for a,b,c being object st R[a,b] & R[a,c] holds b = c
    proof
      let a,b,c be object;
      assume that
A4:   a is Ordinal and
A5:   b is Sequence and
A6:   for A,L st A = a & L = b holds P[A,L] and
      a is Ordinal and
A7:   c is Sequence and
A8:   for A,L st A = a & L = c holds P[ A,L];
      reconsider a as Ordinal by A4;
      reconsider c as Sequence by A7;
A9:   dom c = a by A8;
A10:  for A st A in a & A <> 0 & A is limit_ordinal holds c.A = D(A,c|A)
      by A8;
A11:  for A st succ A in a holds c.(succ A) = C(A,c.A) by A8;
A12:  0 in a implies c.0 = B() by A8;
      reconsider b as Sequence by A5;
A13:  0 in a implies b.0 = B() by A6;
A14:  for A st succ A in a holds b.(succ A) = C(A,b.A) by A6;
A15:  for A st A in a & A <> 0 & A is limit_ordinal holds b.A = D(A,b|A)
      by A6;
A16:  dom b = a by A6;
      b = c from TSUniq1(A16,A13,A14,A15,A9,A12,A11,A10);
      hence thesis;
    end;
    consider G being Function such that
A17: for a,b being object holds [a,b] in G iff a in B & R[a,b]
      from FUNCT_1:sch 1(A3);
    defpred Q[object,object] means
     ex A,L st A = $1 & L = G.$1 & (A = 0 & $2 = B()
or (ex B st A = succ B & $2 = C(B,L.B)) or A <> 0 & A is limit_ordinal & $2 =
    D(A,L));
A18: dom G = B
    proof
      thus for a being object holds  a in dom G implies a in B
      proof let a be object;
        assume a in dom G;
        then ex b being object st [a,b] in G by XTUPLE_0:def 12;
        hence thesis by A17;
      end;
      let a be object;
      assume
A19:  a in B;
      then reconsider a9 = a as Ordinal;
      consider L such that
A20:  P[a9,L] by A2,A19;
      for A holds for K be Sequence holds A = a9 & K = L implies P[A,K]
      by A20;
      then [a9,L] in G by A17,A19;
      hence thesis by XTUPLE_0:def 12;
    end;
A21: for a being object st a in B ex b being object st Q[a,b]
    proof
      let a be object;
      assume
A22:  a in B;
      then reconsider A = a as Ordinal;
      consider c being object such that
A23:  [a,c] in G by A18,A22,XTUPLE_0:def 12;
      reconsider L = c as Sequence by A17,A23;
A24:  now
        given C such that
A25:    A = succ C;
        thus ex b being object st Q[a,b]
        proof
          take C(C,L.C), A, L;
          thus A = a & L = G.a by A23,FUNCT_1:1;
          thus thesis by A25;
        end;
      end;
A26:  now
        assume
A27:    A <> 0 & for C holds A <> succ C;
        thus Q[a,D(A,L)]
        proof
          take A,L;
          thus A = a & L = G.a by A23,FUNCT_1:1;
          thus thesis by A27,ORDINAL1:29;
        end;
      end;
      now
        assume
A28:    A = 0;
        thus Q[a,B()]
        proof
          take A,L;
          thus A = a & L = G.a by A23,FUNCT_1:1;
          thus thesis by A28;
        end;
      end;
      hence thesis by A24,A26;
    end;
A29: for a,b,c being object st a in B & Q[a,b] & Q[a,c] holds b = c
    proof
      let a,b,c being object such that
      a in B;
      given Ab being Ordinal,Lb being Sequence such that
A30:  Ab = a and
A31:  Lb = G.a and
A32:  Ab = 0 & b = B() or (ex B st Ab = succ B & b = C(B,Lb.B)) or
      Ab <> 0 & Ab is limit_ordinal & b = D(Ab,Lb);
      given Ac being Ordinal,Lc being Sequence such that
A33:  Ac = a and
A34:  Lc = G.a and
A35:  Ac = 0 & c = B() or (ex B st Ac = succ B & c = C(B,Lc.B)) or
      Ac <> 0 & Ac is limit_ordinal & c = D(Ac,Lc);
      now
        given C such that
A36:    Ab = succ C;
        consider A such that
A37:    Ab = succ A and
A38:    b = C(A,Lb.A) by A32,A36,ORDINAL1:29;
        consider D such that
A39:    Ac = succ D and
A40:    c = C(D,Lc.D) by A30,A33,A35,A36,ORDINAL1:29;
        A = D by A30,A33,A37,A39,ORDINAL1:7;
        hence thesis by A31,A34,A38,A40;
      end;
      hence thesis by A30,A31,A32,A33,A34,A35;
    end;
    consider F being Function such that
A41: dom F = B & for a being object st a in B holds Q[a,F.a]
from FUNCT_1:sch 2(A29
    ,A21);
    reconsider L = F as Sequence by A41,ORDINAL1:def 7;
    take L;
    thus dom L = B by A41;
    thus 0 in B implies L.0 = B()
    proof
      assume 0 in B;
      then ex A being Ordinal, K being Sequence st A = 0 & K = G.0 & (A =
0 & F.0 = B() or (ex B st A = succ B & F.0 = C(B,K.B)) or A <> 0 & A is
      limit_ordinal & F.0 = D(A,K)) by A41;
      hence thesis;
    end;
A42: for A,L1 st A in B & L1 = G.A holds L|A = L1
    proof
      defpred P[Ordinal] means for L1 st $1 in B & L1 = G.$1 holds L|$1 = L1;
A43:  for A st for C st C in A holds P[C] holds P[A]
      proof
        let A such that
        for C st C in A for L1 st C in B & L1 = G.C holds L|C = L1;
        let L1;
        assume that
A44:    A in B and
A45:    L1 = G.A;
A46:    [A,L1] in G by A18,A44,A45,FUNCT_1:1;
        then
A47:    P[A,L1] by A17;
A48:    now
          let x be object;
          assume
A49:      x in A;
          then reconsider x9 = x as Ordinal;
A50:      x9 in B by A44,A49,ORDINAL1:10;
          then consider A1,L2 such that
A51:      A1 = x9 and
A52:      L2 = G.x9 and
A53:      A1 = 0 & L.x9 = B() or (ex B st A1 = succ B & L.x9 = C(B,
          L2.B)) or A1 <> 0 & A1 is limit_ordinal & L.x9 = D(A1,L2) by A41;
          for D,L3 st D = x9 & L3 = L1|x9 holds P[D,L3]
          proof
            let D,L3 such that
A54:        D = x9 and
A55:        L3 = L1|x9;
            x9 c= A by A49,ORDINAL1:def 2;
            hence dom L3 = D by A47,A54,A55,RELAT_1:62;
            thus 0 in D implies L3.0 = B() by A47,A49,A54,A55,FUNCT_1:49
,ORDINAL1:10;
            thus succ C in D implies L3.(succ C) = C(C,L3.C)
            proof
              assume
A56:          succ C in D;
              C in succ C by ORDINAL1:6;
              then
A57:          L1|x9.C = L1.C by A54,A56,FUNCT_1:49,ORDINAL1:10;
              succ C in A & L1|x9.succ C = L1.succ C by A49,A54,A56,FUNCT_1:49
,ORDINAL1:10;
              hence thesis by A17,A46,A55,A57;
            end;
            let C;
            assume that
A58:        C in D and
A59:        C <> 0 & C is limit_ordinal;
            C c= x9 by A54,A58,ORDINAL1:def 2;
            then
A60:        L1|C = L3|C by A55,FUNCT_1:51;
            C in A by A49,A54,A58,ORDINAL1:10;
            then L1.C = D(C,L3|C) by A17,A46,A59,A60;
            hence thesis by A54,A55,A58,FUNCT_1:49;
          end;
          then [x9,L1|x9] in G by A17,A50;
          then
A61:      L1|x9 = L2 by A52,FUNCT_1:1;
A62:      L|A.x = L.x by A49,FUNCT_1:49;
          now
            given D such that
A63:        x9 = succ D;
A64:        L1.x = C(D,L1.D) by A17,A46,A49,A63;
            consider C such that
A65:        A1 = succ C and
A66:        L.x9 = C(C,L2.C) by A51,A53,A63,ORDINAL1:29;
            C = D by A51,A63,A65,ORDINAL1:7;
            hence L1.x = L|A.x by A62,A61,A63,A66,A64,FUNCT_1:49,ORDINAL1:6;
          end;
          hence L1.x = L|A.x by A17,A46,A49,A51,A53,A62,A61;
        end;
        A c= dom L by A41,A44,ORDINAL1:def 2;
        then dom(L|A) = A by RELAT_1:62;
        hence thesis by A47,A48,FUNCT_1:2;
      end;
      thus for A holds P[A] from ORDINAL1:sch 2(A43);
    end;
    thus succ A in B implies L.(succ A) = C(A,L.A)
    proof
      assume
A67:  succ A in B;
      then consider C being Ordinal, K being Sequence such that
A68:  C = succ A and
A69:  K = G.succ A and
A70:  C = 0 & F.succ A = B() or (ex B st C = succ B & F.succ A = C(B
      ,K.B)) or C <> 0 & C is limit_ordinal & F.succ A = D(C,K) by A41;
A71:  K = L|succ A by A42,A67,A69;
      consider D such that
A72:  C = succ D and
A73:  F.succ A = C(D,K.D) by A68,A70,ORDINAL1:29;
      A = D by A68,A72,ORDINAL1:7;
      hence thesis by A73,A71,FUNCT_1:49,ORDINAL1:6;
    end;
    let D;
    assume that
A74: D in B and
A75: D <> 0 & D is limit_ordinal;
    ex A being Ordinal, K being Sequence st A = D & K = G.D & (A = 0
    & F.D = B() or (ex B st A = succ B & F.D = C(B,K.B)) or A <> 0 & A is
    limit_ordinal & F.D = D(A,K)) by A41,A74;
    hence thesis by A42,A74,A75,ORDINAL1:29;
  end;
  for A holds R[A] from ORDINAL1:sch 2(A1);
  hence thesis;
end;

scheme
  TSResult { L()->Sequence, F(Ordinal)->set, A()->Ordinal, B()->set, C(
Ordinal,set)->set, D(Ordinal,Sequence)->set } : for A st A in dom L() holds L
  ().A = F(A)
provided
A1: for A,x holds x = F(A) iff ex L st x = last L & dom L = succ A & L.
0 = B() & (for C st succ C in succ A holds L.succ C = C(C,L.C)) & for C st C
in succ A & C <> 0 & C is limit_ordinal holds L.C = D(C,L|C) and
A2: dom L() = A() and
A3: 0 in A() implies L().0 = B() and
A4: for A st succ A in A() holds L().(succ A) = C(A,L().A) and
A5: for A st A in A() & A <> 0 & A is limit_ordinal holds L().A = D(A,L ()|A)
proof
  let A;
  set L = L()|succ A;
  assume A in dom L();
  then
A6: succ A c= dom L() by ORDINAL1:21;
A7: for C st succ C in succ A holds L.succ C = C(C,L.C)
  proof
    let C such that
A8: succ C in succ A;
    C in succ C by ORDINAL1:6;
    then
A9: L.C = L().C by A8,FUNCT_1:49,ORDINAL1:10;
    L.succ C = L().succ C by A8,FUNCT_1:49;
    hence thesis by A2,A4,A6,A8,A9;
  end;
A10: for C st C in succ A & C <> 0 & C is limit_ordinal holds L.C = D(C,L|C )
  proof
    let C;
    assume that
A11: C in succ A and
A12: C <> 0 & C is limit_ordinal;
    C c= succ A by A11,ORDINAL1:def 2;
    then
A13: L|C = L()|C by FUNCT_1:51;
    L.C = L().C by A11,FUNCT_1:49;
    hence thesis by A2,A5,A6,A11,A12,A13;
  end;
  0 c= succ A;
  then 0 c< succ A;
  then
A14: 0 in succ A & L.0 = L().0 by FUNCT_1:49,ORDINAL1:11;
A15: dom L = succ A by A6,RELAT_1:62;
  then A in succ A & last L = L.A by Th2,ORDINAL1:21;
  then last L = L().A by FUNCT_1:49;
  hence thesis by A1,A2,A3,A6,A15,A14,A7,A10;
end;

scheme
  TSDef { A()->Ordinal, B()->set, C(Ordinal,set)->set, D(Ordinal,Sequence)->
set } : (ex x,L st x = last L & dom L = succ A() & L.0 = B() & (for C st succ
C in succ A() holds L.succ C = C(C,L.C)) & for C st C in succ A() & C <> 0 & C
is limit_ordinal holds L.C = D(C,L|C) ) & for x1,x2 being set st (ex L st x1 =
last L & dom L = succ A() & L.0 = B() & (for C st succ C in succ A() holds L.
  succ C = C(C,L.C)) & for C st C in succ A() & C <> 0 & C is limit_ordinal
holds L.C = D(C,L|C) ) & (ex L st x2 = last L & dom L = succ A() & L.0 = B() &
(for C st succ C in succ A() holds L.succ C = C(C,L.C)) & for C st C in succ A(
  ) & C <> 0 & C is limit_ordinal holds L.C = D(C,L|C) ) holds x1 = x2 proof
  consider L such that
A1: dom L = succ A() & (0 in succ A() implies L.0 = B() ) & (for C st
succ C in succ A() holds L.(succ C) = C(C,L.C)) & for C st C in succ A() & C <>
  0 & C is limit_ordinal holds L.C = D(C,L|C) from TSExist1;
  thus ex x,L st x = last L & dom L = succ A() & L.0 = B() & (for C st succ C
  in succ A() holds L.succ C = C(C,L.C)) & for C st C in succ A() & C <> 0 & C
  is limit_ordinal holds L.C = D(C,L|C)
  proof
    take x = last L, L;
    thus x = last L & dom L = succ A() by A1;
    0 c= succ A();
    then 0 c< succ A();
    hence thesis by A1,ORDINAL1:11;
  end;
  let x1,x2 be set;
  given L1 such that
A2: x1 = last L1 and
A3: dom L1 = succ A() and
A4: L1.0 = B() and
A5: for C st succ C in succ A() holds L1.succ C = C(C,L1.C) and
A6: for C st C in succ A() & C <> 0 & C is limit_ordinal holds L1.C = D
  (C,L1|C);
A7: 0 in succ A() implies L1.0 = B() by A4;
  given L2 such that
A8: x2 = last L2 and
A9: dom L2 = succ A() and
A10: L2.0 = B() and
A11: for C st succ C in succ A() holds L2.succ C = C(C,L2.C) and
A12: for C st C in succ A() & C <> 0 & C is limit_ordinal holds L2.C =
  D(C,L2|C);
A13: 0 in succ A() implies L2.0 = B() by A10;
  L1 = L2 from TSUniq1(A3,A7,A5,A6,A9,A13,A11,A12);
  hence thesis by A2,A8;
end;

scheme
  TSResult0 { F(Ordinal)->set, B()->set, C(Ordinal,set)->set, D(Ordinal,
  Sequence)->set } : F(0) = B()
provided
A1: for A,x holds x = F(A) iff ex L st x = last L & dom L = succ A & L.
0 = B() & (for C st succ C in succ A holds L.succ C = C(C,L.C)) & for C st C
in succ A & C <> 0 & C is limit_ordinal holds L.C = D(C,L|C)
proof
  consider L such that
A2: dom L = succ 0 & (0 in succ 0 implies L.0 = B() ) & (for A st
succ A in succ 0 holds L.(succ A) = C(A,L.A) ) & for A st A in succ 0 & A <>
  0 & A is limit_ordinal holds L.A = D(A,L|A) from TSExist1;
  B() = last L by A2,Th2,ORDINAL1:6;
  hence thesis by A1,A2,ORDINAL1:6;
end;

scheme
  TSResultS { B()->set, C(Ordinal,set)->set, D(Ordinal,Sequence)->set, F(
  Ordinal)->set } : for A holds F(succ A) = C(A,F(A))
provided
A1: for A,x holds x = F(A) iff ex L st x = last L & dom L = succ A & L.
0 = B() & (for C st succ C in succ A holds L.succ C = C(C,L.C)) & for C st C
in succ A & C <> 0 & C is limit_ordinal holds L.C = D(C,L|C)
proof
  let A;
  consider L such that
A2: dom L = succ succ A and
A3: 0 in succ succ A implies L.0 = B() and
A4: for C st succ C in succ succ A holds L.(succ C) = C(C,L.C) and
A5: for C st C in succ succ A & C <> 0 & C is limit_ordinal holds L.C =
  D(C,L|C) from TSExist1;
A6: for A,x holds x = F(A) iff ex L st x = last L & dom L = succ A & L.0 =
  B() & (for C st succ C in succ A holds L.succ C = C(C,L.C)) & for C st C in
  succ A & C <> 0 & C is limit_ordinal holds L.C = D(C,L|C) by A1;
A7: for B st B in dom L holds L.B = F(B) from TSResult(A6,A2,A3,A4, A5);
  then
A8: L.succ A = F(succ A) by A2,ORDINAL1:6;
  A in succ A & succ A in succ succ A by ORDINAL1:6;
  then L.A = F(A) by A2,A7,ORDINAL1:10;
  hence thesis by A4,A8,ORDINAL1:6;
end;

scheme
  TSResultL { L()->Sequence, A()->Ordinal, F(Ordinal)->set, B()->set, C(
  Ordinal,set)->set, D(Ordinal,Sequence)->set } : F(A()) = D(A(),L())
provided
A1: for A,x holds x = F(A) iff ex L st x = last L & dom L = succ A & L.
0 = B() & (for C st succ C in succ A holds L.succ C = C(C,L.C)) & for C st C
in succ A & C <> 0 & C is limit_ordinal holds L.C = D(C,L|C) and
A2: A() <> 0 & A() is limit_ordinal and
A3: dom L() = A() and
A4: for A st A in A() holds L().A = F(A)
proof
A5: A() in succ A() by ORDINAL1:6;
  consider L such that
A6: dom L = succ A() and
A7: 0 in succ A() implies L.0 = B() and
A8: for C st succ C in succ A() holds L.(succ C) = C(C,L.C) and
A9: for C st C in succ A() & C <> 0 & C is limit_ordinal holds L.C = D(
  C,L|C) from TSExist1;
  set L1 = L|A();
A10: for A,x holds x = F(A) iff ex L st x = last L & dom L = succ A & L.0 =
  B() & (for C st succ C in succ A holds L.succ C = C(C,L.C)) & for C st C in
  succ A & C <> 0 & C is limit_ordinal holds L.C = D(C,L|C) by A1;
A11: for B st B in dom L holds L.B = F(B) from TSResult(A10,A6,A7,A8, A9);
A12: now
    let x be object;
    assume
A13: x in A();
    then reconsider x9 = x as Ordinal;
    thus L1.x = L.x9 by A13,FUNCT_1:49
      .= F(x9) by A6,A11,A5,A13,ORDINAL1:10
      .= L().x by A4,A13;
  end;
  A() c= dom L by A6,A5,ORDINAL1:def 2;
  then dom L1 = A() by RELAT_1:62;
  then L1 = L() by A3,A12,FUNCT_1:2;
  then L.A() = D(A(),L()) by A2,A9,ORDINAL1:6;
  hence thesis by A6,A11,ORDINAL1:6;
end;

scheme
  OSExist { A()->Ordinal, B()->Ordinal, C(Ordinal,Ordinal)->Ordinal, D(Ordinal
,Sequence)->Ordinal } : ex fi st dom fi = A() & (0 in A() implies fi.0 = B(
) ) & (for A st succ A in A() holds fi.(succ A) = C(A,fi.A) ) & for A st A in A
  () & A <> 0 & A is limit_ordinal holds fi.A = D(A,fi|A) proof
  deffunc CC(Ordinal,set) = C($1,sup union {$2});
  consider L such that
A1: dom L = A() and
A2: 0 in A() implies L.0 = B() and
A3: for A st succ A in A() holds L.(succ A) = CC(A,L.A) and
A4: for A st A in A() & A <> 0 & A is limit_ordinal holds L.A = D(A,L|A
  ) from TSExist1;
  L is Ordinal-yielding
  proof
    take sup rng L;
    let x be object;
    assume
A5: x in rng L;
    then consider y being object such that
A6: y in dom L and
A7: x = L.y by FUNCT_1:def 3;
    reconsider y as Ordinal by A6;
A8: now
      assume that
A9:   y <> 0 and
A10:  for B holds y <> succ B;
      y is limit_ordinal by A10,ORDINAL1:29;
      then L.y = D(y,L|y) by A1,A4,A6,A9;
      hence x is Ordinal by A7;
    end;
A11: On rng L c= sup rng L by Def3;
    now
      given B such that
A12:  y = succ B;
      L.y = C(B,sup union {L.B}) by A1,A3,A6,A12;
      hence x is Ordinal by A7;
    end;
    then x in On rng L by A1,A2,A5,A6,A7,A8,ORDINAL1:def 9;
    hence thesis by A11;
  end;
  then reconsider L as Ordinal-Sequence;
  take fi = L;
  thus dom fi = A() & (0 in A() implies fi.0 = B() ) by A1,A2;
  thus for A st succ A in A() holds fi.(succ A) = C(A,fi.A)
  proof
    let A;
    reconsider B = fi.A as Ordinal;
    sup union {B} = sup B by ZFMISC_1:25
      .= B by Th18;
    hence thesis by A3;
  end;
  thus thesis by A4;
end;

scheme
  OSResult { fi()->Ordinal-Sequence, F(Ordinal)->Ordinal, A()->Ordinal, B()->
Ordinal, C(Ordinal,Ordinal)->Ordinal, D(Ordinal,Sequence)->Ordinal } : for A
  st A in dom fi() holds fi().A = F(A)
provided
A1: for A,B holds B = F(A) iff ex fi st B = last fi & dom fi = succ A &
fi.0 = B() & (for C st succ C in succ A holds fi.succ C = C(C,fi.C)) & for C
st C in succ A & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) and
A2: dom fi() = A() and
A3: 0 in A() implies fi().0 = B() and
A4: for A st succ A in A() holds fi().(succ A) = C(A,fi().A) and
A5: for A st A in A() & A <> 0 & A is limit_ordinal holds fi().A = D(A,
fi()|A)
proof
  let A;
  set fi = fi()|succ A;
  assume A in dom fi();
  then
A6: succ A c= dom fi() by ORDINAL1:21;
A7: for C st succ C in succ A holds fi.succ C = C(C,fi.C)
  proof
    let C such that
A8: succ C in succ A;
    C in succ C by ORDINAL1:6;
    then
A9: fi.C = fi().C by A8,FUNCT_1:49,ORDINAL1:10;
    fi.succ C = fi().succ C by A8,FUNCT_1:49;
    hence thesis by A2,A4,A6,A8,A9;
  end;
A10: for C st C in succ A & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi
  |C)
  proof
    let C;
    assume that
A11: C in succ A and
A12: C <> 0 & C is limit_ordinal;
    C c= succ A by A11,ORDINAL1:def 2;
    then
A13: fi|C = fi()|C by FUNCT_1:51;
    fi.C = fi().C by A11,FUNCT_1:49;
    hence thesis by A2,A5,A6,A11,A12,A13;
  end;
  0 c= succ A;
  then 0 c< succ A;
  then
A14: 0 in succ A & fi.0 = fi().0 by FUNCT_1:49,ORDINAL1:11;
A15: dom fi = succ A by A6,RELAT_1:62;
  then A in succ A & last fi = fi.A by Th2,ORDINAL1:21;
  then last fi = fi().A by FUNCT_1:49;
  hence thesis by A1,A2,A3,A6,A15,A14,A7,A10;
end;

scheme
  OSDef { A()->Ordinal, B()->Ordinal, C(Ordinal,Ordinal)->Ordinal, D(Ordinal,
Sequence)->Ordinal } : (ex A,fi st A = last fi & dom fi = succ A() & fi.0 =
B() & (for C st succ C in succ A() holds fi.succ C = C(C,fi.C)) & for C st C in
succ A() & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) ) & for A1,A2 st
(ex fi st A1 = last fi & dom fi = succ A() & fi.0 = B() & (for C st succ C in
succ A() holds fi.succ C = C(C,fi.C)) & for C st C in succ A() & C <> 0 & C is
limit_ordinal holds fi.C = D(C,fi|C) ) & (ex fi st A2 = last fi & dom fi = succ
A() & fi.0 = B() & (for C st succ C in succ A() holds fi.succ C = C(C,fi.C)) &
for C st C in succ A() & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) )
  holds A1 = A2 proof
  consider fi such that
A1: dom fi = succ A() & (0 in succ A() implies fi.0 = B() ) & (for C
st succ C in succ A() holds fi.(succ C) = C(C,fi.C)) & for C st C in succ A() &
  C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) from OSExist;
  reconsider A = last fi as Ordinal;
  thus ex A,fi st A = last fi & dom fi = succ A() & fi.0 = B() & (for C st
succ C in succ A() holds fi.succ C = C(C,fi.C)) & for C st C in succ A() & C <>
  0 & C is limit_ordinal holds fi.C = D(C,fi|C)
  proof
    take A, fi;
    thus A = last fi & dom fi = succ A() by A1;
    0 c= succ A();
    then 0 c< succ A();
    hence thesis by A1,ORDINAL1:11;
  end;
  deffunc CD(Ordinal,Ordinal) = C($1,sup union { $2 });
  let A1,A2 be Ordinal;
  given L1 being Ordinal-Sequence such that
A2: A1 = last L1 and
A3: dom L1 = succ A() and
A4: L1.0 = B() and
A5: for C st succ C in succ A() holds L1.succ C = C(C,L1.C) and
A6: for C st C in succ A() & C <> 0 & C is limit_ordinal holds L1.C = D
  (C,L1|C);
A7: 0 in succ A() implies L1.0 = B() by A4;
A8: for C st succ C in succ A() holds L1.(succ C) = CD(C,L1.C)
  proof
    let C such that
A9: succ C in succ A();
    reconsider x9 = L1.C as Ordinal;
    sup union { L1.C } = sup x9 by ZFMISC_1:25
      .= x9 by Th18;
    hence thesis by A5,A9;
  end;
  given L2 being Ordinal-Sequence such that
A10: A2 = last L2 and
A11: dom L2 = succ A() and
A12: L2.0 = B() and
A13: for C st succ C in succ A() holds L2.succ C = C(C,L2.C) and
A14: for C st C in succ A() & C <> 0 & C is limit_ordinal holds L2.C =
  D(C,L2|C);
A15: for C st C in succ A() & C <> 0 & C is limit_ordinal holds L2.C = D(C,
  L2|C) by A14;
A16: for C st C in succ A() & C <> 0 & C is limit_ordinal holds L1.C = D(C,
  L1|C) by A6;
A17: for C st succ C in succ A() holds L2.(succ C) = CD(C,L2.C)
  proof
    let C such that
A18: succ C in succ A();
    reconsider x9 = L2.C as Ordinal;
    sup union { L2.C } = sup x9 by ZFMISC_1:25
      .= x9 by Th18;
    hence thesis by A13,A18;
  end;
A19: 0 in succ A() implies L2.0 = B() by A12;
  L1 = L2 from TSUniq1(A3,A7,A8,A16,A11,A19,A17,A15);
  hence thesis by A2,A10;
end;

scheme
  OSResult0 { F(Ordinal)->Ordinal, B()->Ordinal, C(Ordinal,Ordinal)->Ordinal,
  D(Ordinal,Sequence)->Ordinal } : F(0) = B()
provided
A1: for A,B holds B = F(A) iff ex fi st B = last fi & dom fi = succ A &
fi.0 = B() & (for C st succ C in succ A holds fi.succ C = C(C,fi.C)) & for C
st C in succ A & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C)
proof
  consider fi such that
A2: dom fi = succ 0 & (0 in succ 0 implies fi.0 = B() ) & (for A st
  succ A in succ 0 holds fi.(succ A) = C(A,fi.A) ) & for A st A in succ 0 & A
  <> 0 & A is limit_ordinal holds fi.A = D(A,fi|A) from OSExist;
  B() = last fi by A2,Th2,ORDINAL1:6;
  hence thesis by A1,A2,ORDINAL1:6;
end;

scheme
  OSResultS { B()->Ordinal, C(Ordinal,Ordinal)->Ordinal, D(Ordinal,Sequence)
  ->Ordinal, F(Ordinal)->Ordinal } : for A holds F(succ A) = C(A,F(A))
provided
A1: for A,B holds B = F(A) iff ex fi st B = last fi & dom fi = succ A &
fi.0 = B() & (for C st succ C in succ A holds fi.succ C = C(C,fi.C)) & for C
st C in succ A & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C)
proof
  let A;
  consider fi such that
A2: dom fi = succ succ A and
A3: 0 in succ succ A implies fi.0 = B() and
A4: for C st succ C in succ succ A holds fi.(succ C) = C(C,fi.C) and
A5: for C st C in succ succ A & C <> 0 & C is limit_ordinal holds fi.C
  = D(C,fi|C) from OSExist;
A6: for A,B holds B = F(A) iff ex fi st B = last fi & dom fi = succ A & fi.
0 = B() & (for C st succ C in succ A holds fi.succ C = C(C,fi.C)) & for C st C
  in succ A & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by A1;
A7: for B st B in dom fi holds fi.B = F(B) from OSResult(A6,A2,A3,A4, A5);
  then
A8: fi.succ A = F(succ A) by A2,ORDINAL1:6;
  A in succ A & succ A in succ succ A by ORDINAL1:6;
  then fi.A = F(A) by A2,A7,ORDINAL1:10;
  hence thesis by A4,A8,ORDINAL1:6;
end;

scheme
  OSResultL { fi()->Ordinal-Sequence, A()->Ordinal, F(Ordinal)->Ordinal, B()->
Ordinal, C(Ordinal,Ordinal)->Ordinal, D(Ordinal,Sequence)->Ordinal } : F(A())
  = D(A(),fi())
provided
A1: for A,B holds B = F(A) iff ex fi st B = last fi & dom fi = succ A &
fi.0 = B() & (for C st succ C in succ A holds fi.succ C = C(C,fi.C)) & for C
st C in succ A & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) and
A2: A() <> 0 & A() is limit_ordinal and
A3: dom fi() = A() and
A4: for A st A in A() holds fi().A = F(A)
proof
A5: A() in succ A() by ORDINAL1:6;
  consider fi such that
A6: dom fi = succ A() and
A7: 0 in succ A() implies fi.0 = B() and
A8: for C st succ C in succ A() holds fi.(succ C) = C(C,fi.C) and
A9: for C st C in succ A() & C <> 0 & C is limit_ordinal holds fi.C = D
  (C,fi|C) from OSExist;
  set psi = fi|A();
A10: for A,B holds B = F(A) iff ex fi st B = last fi & dom fi = succ A & fi.
0 = B() & (for C st succ C in succ A holds fi.succ C = C(C,fi.C)) & for C st C
  in succ A & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by A1;
A11: for B st B in dom fi holds fi.B = F(B) from OSResult(A10,A6,A7,A8, A9);
A12: now
    let x be object;
    assume
A13: x in A();
    then reconsider x9 = x as Ordinal;
    thus psi.x = fi.x9 by A13,FUNCT_1:49
      .= F(x9) by A6,A11,A5,A13,ORDINAL1:10
      .= fi().x by A4,A13;
  end;
  A() c= dom fi by A6,A5,ORDINAL1:def 2;
  then dom psi = A() by RELAT_1:62;
  then psi = fi() by A3,A12,FUNCT_1:2;
  then fi.A() = D(A(),fi()) by A2,A9,ORDINAL1:6;
  hence thesis by A6,A11,ORDINAL1:6;
end;

definition
  let L;
  func sup L -> Ordinal equals
  sup rng L;
  correctness;
  func inf L -> Ordinal equals
  inf rng L;
  correctness;
end;

theorem
  sup L = sup rng L & inf L = inf rng L;

definition
  let L;
  func lim_sup L -> Ordinal means
  ex fi st it = inf fi & dom fi = dom L & for
  A st A in dom L holds fi.A = sup rng (L|(dom L \ A));
  existence
  proof
    deffunc F(Ordinal) = sup rng (L|(dom L \ $1));
    consider fi such that
A1: dom fi = dom L & for A st A in dom L holds fi.A = F(A) from
    OSLambda;
    take inf fi, fi;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let A1,A2 be Ordinal;
    given fi such that
A2: A1 = inf fi & dom fi = dom L and
A3: for A st A in dom L holds fi.A = sup rng (L|(dom L \ A));
    given psi such that
A4: A2 = inf psi & dom psi = dom L and
A5: for A st A in dom L holds psi.A = sup rng (L|(dom L \ A));
    now
      let x be object;
      assume
A6:   x in dom L;
      then reconsider A = x as Ordinal;
      fi.A = sup rng (L|(dom L \ A)) by A3,A6;
      hence fi.x = psi.x by A5,A6;
    end;
    hence thesis by A2,A4,FUNCT_1:2;
  end;
  func lim_inf L -> Ordinal means
  ex fi st it = sup fi & dom fi = dom L & for
  A st A in dom L holds fi.A = inf rng (L|(dom L \ A));
  existence
  proof
    deffunc F(Ordinal) = inf rng (L|(dom L \ $1));
    consider fi such that
A7: dom fi = dom L & for A st A in dom L holds fi.A = F(A) from
    OSLambda;
    take sup fi, fi;
    thus thesis by A7;
  end;
  uniqueness
  proof
    let A1,A2 be Ordinal;
    given fi such that
A8: A1 = sup fi & dom fi = dom L and
A9: for A st A in dom L holds fi.A = inf rng (L|(dom L \ A));
    given psi such that
A10: A2 = sup psi & dom psi = dom L and
A11: for A st A in dom L holds psi.A = inf rng (L|(dom L \ A));
    now
      let x be object;
      assume
A12:  x in dom L;
      then reconsider A = x as Ordinal;
      fi.A = inf rng (L|(dom L \ A)) by A9,A12;
      hence fi.x = psi.x by A11,A12;
    end;
    hence thesis by A8,A10,FUNCT_1:2;
  end;
end;

definition
  let A,fi;
  pred A is_limes_of fi means
  :Def9:
  ex B st B in dom fi & for C st B c= C &
C in dom fi holds fi.C = 0 if A = 0 otherwise for B,C st B in A & A in C ex D
st D in dom fi & for E being Ordinal st D c= E & E in dom fi holds B in fi.E &
  fi.E in C;
  consistency;
end;

definition
  let fi;
  given A such that
A1: A is_limes_of fi;
  func lim fi -> Ordinal means
  :Def10:
  it is_limes_of fi;
  existence by A1;
  uniqueness
  proof
    let A1,A2 be Ordinal such that
A2: (A1 = 0 & ex B st B in dom fi & for C st B c= C & C in dom fi
holds fi.C = 0) or (A1 <> 0 & for B,C st B in A1 & A1 in C ex D st D in dom
fi & for E being Ordinal st D c= E & E in dom fi holds B in fi.E & fi.E in C)
    and
A3: (A2 = 0 & ex B st B in dom fi & for C st B c= C & C in dom fi
holds fi.C = 0) or (A2 <> 0 & for B,C st B in A2 & A2 in C ex D st D in dom
fi & for E being Ordinal st D c= E & E in dom fi holds B in fi.E & fi.E in C);
A4: now
      set x = the Element of A1;
      reconsider x as Ordinal;
      assume A1 in A2;
      then consider D such that
A5:   D in dom fi and
A6:   for A st D c= A & A in dom fi holds A1 in fi.A & fi.A in succ A2
      by A3,ORDINAL1:6;
      now
        assume A1 = 0;
        then consider B such that
A7:     B in dom fi and
A8:     for C st B c= C & C in dom fi holds fi.C = 0 by A2;
        B c= D or D c= B;
        then consider E being Ordinal such that
A9:     E = D & B c= D or E = B & D c= B;
        fi.E = 0 by A5,A7,A8,A9;
        hence contradiction by A5,A6,A7,A9;
      end;
      then consider C such that
A10:  C in dom fi and
A11:  for A st C c= A & A in dom fi holds x in fi.A & fi.A in succ A1
      by A2,ORDINAL1:6;
      C c= D or D c= C;
      then consider E being Ordinal such that
A12:  E = D & C c= D or E = C & D c= C;
      fi.E in succ A1 by A5,A10,A11,A12;
      then
A13:  fi.E in A1 or fi.E = A1 by ORDINAL1:8;
      A1 in fi.E by A5,A6,A10,A12;
      hence contradiction by A13;
    end;
    set x = the Element of A2;
    reconsider x as Ordinal;
    assume A1 <> A2;
    then A1 in A2 or A2 in A1 by ORDINAL1:14;
    then consider D such that
A14: D in dom fi and
A15: for A st D c= A & A in dom fi holds A2 in fi.A & fi.A in succ A1
    by A2,A4,ORDINAL1:6;
    now
      assume A2 = 0;
      then consider B such that
A16:  B in dom fi and
A17:  for C st B c= C & C in dom fi holds fi.C = 0 by A3;
      B c= D or D c= B;
      then consider E being Ordinal such that
A18:  E = D & B c= D or E = B & D c= B;
      fi.E = 0 by A14,A16,A17,A18;
      hence contradiction by A14,A15,A16,A18;
    end;
    then consider C such that
A19: C in dom fi and
A20: for A st C c= A & A in dom fi holds x in fi.A & fi.A in succ A2
    by A3,ORDINAL1:6;
    C c= D or D c= C;
    then consider E being Ordinal such that
A21: E = D & C c= D or E = C & D c= C;
    fi.E in succ A2 by A14,A19,A20,A21;
    then
A22: fi.E in A2 or fi.E = A2 by ORDINAL1:8;
    A2 in fi.E by A14,A15,A19,A21;
    hence contradiction by A22;
  end;
end;

definition
  let A,fi;
  func lim(A,fi) -> Ordinal equals
  lim(fi|A);
  correctness;
end;

definition
  let L be Ordinal-Sequence;
  attr L is increasing means
  for A,B st A in B & B in dom L holds L.A in L.B;
  attr L is continuous means
  for A,B st A in dom L & A <> 0 & A is
  limit_ordinal & B = L.A holds B is_limes_of L|A;
end;

definition
  let A,B be Ordinal;
  func A +^ B -> Ordinal means
  :Def14:
  ex fi st it = last fi & dom fi = succ B
& fi.0 = A & (for C st succ C in succ B holds fi.succ C = succ(fi.C)) & for C
  st C in succ B & C <> 0 & C is limit_ordinal holds fi.C = sup(fi|C);
  correctness
  proof
    deffunc D(Ordinal,Sequence) = sup $2;
    deffunc C(Ordinal,Ordinal) = succ $2;
    (ex F being Ordinal,fi st F = last fi & dom fi = succ B & fi.0 = A &
(for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C in succ B
& C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) ) & for A1,A2 st (ex fi
    st A1 = last fi & dom fi = succ B & fi.0 = A & (for C st succ C in succ B
    holds fi.succ C = C(C,fi.C)) & for C st C in succ B & C <> 0 & C is
limit_ordinal holds fi.C = D(C,fi|C) ) & (ex fi st A2 = last fi & dom fi = succ
B & fi.0 = A & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C
st C in succ B & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) ) holds A1
    = A2 from OSDef;
    hence thesis;
  end;
end;

definition
  let A,B;
  func A *^ B -> Ordinal means
  :Def15:
  ex fi st it = last fi & dom fi = succ A
& fi.0 = 0 & (for C st succ C in succ A holds fi.succ C = (fi.C)+^B) & for C
  st C in succ A & C <> 0 & C is limit_ordinal holds fi.C = union sup(fi|C);
  correctness
  proof
    deffunc D(Ordinal,Ordinal-Sequence) = union sup $2;
    deffunc C(Ordinal,Ordinal) = $2+^B;
    (ex F being Ordinal,fi st F = last fi & dom fi = succ A & fi.0 = 0 &
(for C st succ C in succ A holds fi.succ C = C(C,fi.C)) & for C st C in succ A
& C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) ) & for A1,A2 st (ex fi
    st A1 = last fi & dom fi = succ A & fi.0 = 0 & (for C st succ C in succ A
    holds fi.succ C = C(C,fi.C)) & for C st C in succ A & C <> 0 & C is
limit_ordinal holds fi.C = D(C,fi|C) ) & (ex fi st A2 = last fi & dom fi = succ
A & fi.0 = 0 & (for C st succ C in succ A holds fi.succ C = C(C,fi.C)) & for
C st C in succ A & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) ) holds
    A1 = A2 from OSDef;
    hence thesis;
  end;
end;

registration
  let O be Ordinal;
  cluster -> ordinal for Element of O;
  coherence;
end;

definition
  let A,B;
  func exp(A,B) -> Ordinal means
  :Def16:
  ex fi st it = last fi & dom fi = succ
B & fi.0 = 1 & (for C st succ C in succ B holds fi.succ C = A*^(fi.C)) & for C
  st C in succ B & C <> 0 & C is limit_ordinal holds fi.C = lim(fi|C);
  correctness
  proof
    deffunc D(Ordinal,Ordinal-Sequence) = lim $2;
    deffunc C(Ordinal,Ordinal) = A*^$2;
    (ex F being Ordinal,fi st F = last fi & dom fi = succ B & fi.0 = 1 &
(for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C in succ B
& C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) ) & for A1,A2 st (ex fi
    st A1 = last fi & dom fi = succ B & fi.0 = 1 & (for C st succ C in succ B
    holds fi.succ C = C(C,fi.C)) & for C st C in succ B & C <> 0 & C is
limit_ordinal holds fi.C = D(C,fi|C) ) & (ex fi st A2 = last fi & dom fi = succ
B & fi.0 = 1 & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C
st C in succ B & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) ) holds A1
    = A2 from OSDef;
    hence thesis;
  end;
end;

theorem Th27:
  A+^0 = A
proof
  deffunc C(Ordinal,Ordinal) = succ $2;
  deffunc D(Ordinal,Sequence) = sup $2;
  deffunc F(Ordinal) = A+^$1;
A1: for B,C holds C = F(B) iff ex fi st C = last fi & dom fi = succ B & fi.
  0 = A & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C
  in succ B & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by Def14;
  thus F(0) = A from OSResult0(A1);
end;

theorem Th28:
  A+^succ B = succ(A+^B)
proof
  deffunc C(Ordinal,Ordinal) = succ $2;
  deffunc D(Ordinal,Sequence) = sup $2;
  deffunc F(Ordinal) = A+^$1;
A1: for B,C holds C = F(B) iff ex fi st C = last fi & dom fi = succ B & fi.
  0 = A & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C
  in succ B & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by Def14;
  for B holds F(succ B) = C(B,F(B)) from OSResultS(A1);
  hence thesis;
end;

theorem Th29:
  B <> 0 & B is limit_ordinal implies for fi st dom fi = B & for
  C st C in B holds fi.C = A+^C holds A+^B = sup fi
proof
  deffunc C(Ordinal,Ordinal) = succ $2;
  deffunc D(Ordinal,Ordinal-Sequence) = sup $2;
  assume
A1: B <> 0 & B is limit_ordinal;
  deffunc F(Ordinal) = A+^$1;
  let fi such that
A2: dom fi = B and
A3: for C st C in B holds fi.C = F(C);
A4: for B,C holds C = F(B) iff ex fi st C = last fi & dom fi = succ B & fi.
  0 = A & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C
  in succ B & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by Def14;
  thus F(B) = D(B,fi) from OSResultL(A4,A1,A2,A3);
end;

theorem Th30:
  0+^A = A
proof
  defpred P[Ordinal] means 0+^$1 = $1;
A1: for A holds P[A] implies P[succ A] by Th28;
A2: for A st A <> 0 & A is limit_ordinal & for B st B in A holds P[B] holds
  P[A]
  proof
    deffunc F(Ordinal) = 0+^$1;
    let A;
    assume that
A3: A <> 0 & A is limit_ordinal and
A4: for B st B in A holds 0+^B = B;
    consider fi such that
A5: dom fi = A & for B st B in A holds fi.B = F(B) from OSLambda;
A6: rng fi = A
    proof
      thus for x being object holds  x in rng fi implies x in A
      proof let x be object;
        assume x in rng fi;
        then consider y being object such that
A7:     y in dom fi and
A8:     x = fi.y by FUNCT_1:def 3;
        reconsider y as Ordinal by A7;
        x = 0+^y by A5,A7,A8
          .= y by A4,A5,A7;
        hence thesis by A5,A7;
      end;
      let x be object;
      assume
A9:   x in A;
      then reconsider B = x as Ordinal;
      0+^B = B & fi.B = 0+^B by A4,A5,A9;
      hence thesis by A5,A9,FUNCT_1:def 3;
    end;
    0+^A = sup fi by A3,A5,Th29
      .= sup rng fi;
    hence thesis by A6,Th18;
  end;
A10: P[0] by Th27;
  for A holds P[A] from OrdinalInd(A10,A1,A2);
  hence thesis;
end;

Lm1: 1 = succ 0;

theorem
  A+^1 = succ A
proof
  thus A+^1 = succ(A+^0) by Lm1,Th28
    .= succ A by Th27;
end;

theorem Th32:
  A in B implies C +^ A in C +^ B
proof
  defpred P[Ordinal] means A in $1 implies C +^ A in C +^ $1;
A1: for B st for D st D in B holds P[D] holds P[B]
  proof
    let B such that
A2: for D st D in B holds A in D implies C +^ A in C +^ D and
A3: A in B;
A4: now
      given D such that
A5:   B = succ D;
A6:   now
        assume A in D;
        then
A7:     C +^ A in C +^ D by A2,A5,ORDINAL1:6;
        succ(C +^ D) = C +^ succ D & C +^ D in succ(C +^ D) by Th28,ORDINAL1:6;
        hence thesis by A5,A7,ORDINAL1:10;
      end;
      now
        assume
A8:     not A in D;
        A c< D iff A c= D & A <> D;
        then C +^ A in succ(C +^ D) by A3,A5,A8,ORDINAL1:11,22;
        hence thesis by A5,Th28;
      end;
      hence thesis by A6;
    end;
    now
      deffunc F(Ordinal) = C+^$1;
      consider fi such that
A9:   dom fi = B & for D st D in B holds fi.D = F(D) from OSLambda;
      fi.A = C+^A by A3,A9;
      then
A10:  C+^A in rng fi by A3,A9,FUNCT_1:def 3;
      assume for D holds B <> succ D;
      then B is limit_ordinal by ORDINAL1:29;
      then C+^B = sup fi by A3,A9,Th29
        .= sup rng fi;
      hence thesis by A10,Th19;
    end;
    hence thesis by A4;
  end;
  for B holds P[B] from ORDINAL1:sch 2(A1);
  hence thesis;
end;

theorem Th33:
  A c= B implies C +^ A c= C +^ B
proof
  assume
A1: A c= B;
  now
    assume A <> B;
    then A c< B by A1;
    then C +^ A in C +^ B by Th32,ORDINAL1:11;
    hence thesis by ORDINAL1:def 2;
  end;
  hence thesis;
end;

theorem Th34:
  A c= B implies A +^ C c= B +^ C
proof
  defpred P[Ordinal] means A +^ $1 c= B +^ $1;
  assume
A1: A c= B;
A2: for C st for D st D in C holds P[D] holds P[C]
  proof
    let C such that
A3: for D st D in C holds A +^ D c= B +^ D;
A4: now
      given D such that
A5:   C = succ D;
A6:   B +^ C = succ(B +^ D) by A5,Th28;
      A +^ D c= B +^ D & A +^ C = succ(A +^ D) by A3,A5,Th28,ORDINAL1:6;
      hence thesis by A6,Th1;
    end;
A7: now
      deffunc F(Ordinal) = A+^$1;
      assume that
A8:   C <> 0 and
A9:   for D holds C <> succ D;
      consider fi such that
A10:  dom fi = C & for D st D in C holds fi.D = F(D) from OSLambda;
A11:  now
        let D;
        assume D in rng fi;
        then consider x being object such that
A12:    x in dom fi and
A13:    D = fi.x by FUNCT_1:def 3;
        reconsider x as Ordinal by A12;
A14:    B +^ x in B +^ C by A10,A12,Th32;
        D = A+^x & A +^ x c= B +^ x by A3,A10,A12,A13;
        hence D in B +^ C by A14,ORDINAL1:12;
      end;
      C is limit_ordinal by A9,ORDINAL1:29;
      then A+^C = sup fi by A8,A10,Th29
        .= sup rng fi;
      hence thesis by A11,Th20;
    end;
    now
      assume
A15:  C = 0;
      then A +^ C = A by Th27;
      hence thesis by A1,A15,Th27;
    end;
    hence thesis by A4,A7;
  end;
  for C holds P[C] from ORDINAL1:sch 2(A2);
  hence thesis;
end;

theorem Th35:
  0*^A = 0
proof
  deffunc D(Ordinal,Sequence) = union sup $2;
  deffunc F(Ordinal) = $1*^A;
  deffunc C(Ordinal,Ordinal) = $2+^A;
A1: for B,C holds C = F(B) iff ex fi st C = last fi & dom fi = succ B & fi.
0 = 0 & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C
  in succ B & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by Def15;
  thus F(0) = 0 from OSResult0(A1);
end;

theorem Th36:
  (succ B)*^A = B*^A +^ A
proof
  deffunc D(Ordinal,Sequence) = union sup $2;
  deffunc F(Ordinal) = $1*^A;
  deffunc C(Ordinal,Ordinal) = $2 +^ A;
A1: for B,C holds C = F(B) iff ex fi st C = last fi & dom fi = succ B & fi.
0 = 0 & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C
  in succ B & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by Def15;
  for B holds F(succ B) = C(B,F(B)) from OSResultS(A1);
  hence thesis;
end;

theorem Th37:
  B <> 0 & B is limit_ordinal implies for fi st dom fi = B & for
  C st C in B holds fi.C = C*^A holds B*^A = union sup fi
proof
  deffunc D(Ordinal,Ordinal-Sequence) = union sup $2;
  assume
A1: B <> 0 & B is limit_ordinal;
  deffunc C(Ordinal,Ordinal) = $2+^A;
  deffunc F(Ordinal) = $1*^A;
  let fi such that
A2: dom fi = B and
A3: for C st C in B holds fi.C = F(C);
A4: for B,C holds C = F(B) iff ex fi st C = last fi & dom fi = succ B & fi.
0 = 0 & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C
  in succ B & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by Def15;
  thus F(B) = D(B,fi) from OSResultL(A4,A1,A2,A3);
end;

theorem Th38:
  A*^0 = 0
proof
  defpred P[Ordinal] means $1*^0 = 0;
A1: for A st P[A] holds P[succ A]
  proof
    let A;
    assume A*^0 = 0;
    hence (succ A)*^0 = 0+^0 by Th36
      .= 0 by Th27;
  end;
A2: for A st A <> 0 & A is limit_ordinal & for B st B in A holds P[B] holds
  P[A]
  proof
    deffunc F(Ordinal) = $1*^0;
    let A;
    assume that
A3: A <> 0 and
A4: A is limit_ordinal and
A5: for B st B in A holds B*^0 = 0;
    consider fi such that
A6: dom fi = A & for B st B in A holds fi.B = F(B) from OSLambda;
    rng fi = succ 0
    proof
      thus for x being object holds  x in rng fi implies x in succ 0
      proof let x be object;
        assume x in rng fi;
        then consider y being object such that
A7:     y in dom fi and
A8:     x = fi.y by FUNCT_1:def 3;
        reconsider y as Ordinal by A7;
        x = y*^0 by A6,A7,A8
          .= 0 by A5,A6,A7;
        hence thesis by TARSKI:def 1;
      end;
      let x be object;
      assume x in succ 0;
      then
A9:   x = 0 by TARSKI:def 1;
      0 c= A;
      then
A10:  0 c< A by A3;
      then
A11:  0 in A by ORDINAL1:11;
      0 *^ 0 = 0 by Th35;
      then fi.x = x by A6,A10,A9,ORDINAL1:11;
      hence thesis by A6,A11,A9,FUNCT_1:def 3;
    end;
    then
A12: sup rng fi = succ 0 by Th18;
    A*^0 = union sup fi by A3,A4,A6,Th37
      .= union sup rng fi;
    hence thesis by A12,Th2;
  end;
A13: P[0] by Th35;
  for A holds P[A] from OrdinalInd(A13,A1,A2);
  hence thesis;
end;

theorem Th39:
  1*^A = A & A*^1 = A
proof
  defpred P[Ordinal] means $1*^succ 0 = $1;
  thus 1*^A = 0*^A +^ A by Lm1,Th36
    .= 0 +^ A by Th35
    .= A by Th30;
A1: for A st for B st B in A holds P[B] holds P[A]
  proof
    let A such that
A2: for B st B in A holds B*^(succ 0) = B;
A3: now
      deffunc F(Ordinal) = $1*^succ 0;
      assume that
A4:   A <> 0 and
A5:   for B holds A <> succ B;
      consider fi such that
A6:   dom fi = A & for D st D in A holds fi.D = F(D) from OSLambda;
A7:   A = rng fi
      proof
        thus A c= rng fi
        proof
          let x be object;
          assume
A8:       x in A;
          then reconsider B = x as Ordinal;
          x = B*^succ 0 by A2,A8
            .= fi.x by A6,A8;
          hence thesis by A6,A8,FUNCT_1:def 3;
        end;
        let x be object;
        assume x in rng fi;
        then consider y being object such that
A9:     y in dom fi and
A10:    x = fi.y by FUNCT_1:def 3;
        reconsider y as Ordinal by A9;
        fi.y = y*^succ 0 by A6,A9
          .= y by A2,A6,A9;
        hence thesis by A6,A9,A10;
      end;
A11:  A is limit_ordinal by A5,ORDINAL1:29;
      then A*^succ 0 = union sup fi by A4,A6,Th37
        .= union sup rng fi;
      hence A*^succ 0 = union A by A7,Th18
        .= A by A11;
    end;
    now
      given B such that
A12:  A = succ B;
      thus A*^(succ 0) = B*^(succ 0) +^ succ 0 by A12,Th36
        .= B +^ succ 0 by A2,A12,ORDINAL1:6
        .= succ(B +^ 0) by Th28
        .= A by A12,Th27;
    end;
    hence thesis by A3,Th35;
  end;
  for A holds P[A] from ORDINAL1:sch 2(A1);
  hence thesis;
end;

theorem Th40:
  C <> 0 & A in B implies A*^C in B*^C
proof
A1: 0 c= C;
  defpred P[Ordinal] means A in $1 implies A*^C in $1*^C;
  assume C <> 0;
  then
A2: 0 c< C by A1;
  then
A3: 0 in C by ORDINAL1:11;
A4: for B st for D st D in B holds P[D] holds P[B]
  proof
    let B such that
A5: for D st D in B holds A in D implies A *^ C in D *^ C and
A6: A in B;
A7: now
      given D such that
A8:   B = succ D;
A9:   now
        assume A in D;
        then
A10:    A*^C in D*^C by A5,A8,ORDINAL1:6;
A11:    D*^C +^ 0 in D*^C +^ C by A2,Th32,ORDINAL1:11;
        D*^C +^ C = (succ D)*^C & D*^C +^ 0 = D*^C by Th27,Th36;
        hence thesis by A8,A10,A11,ORDINAL1:10;
      end;
      now
A12:    A*^C +^ 0 = A*^C by Th27;
        assume
A13:    not A in D;
        A c< D iff A c= D & A <> D;
        then A*^C +^ 0 in D*^C +^ C by A3,A6,A8,A13,Th32,ORDINAL1:11,22;
        hence thesis by A8,A12,Th36;
      end;
      hence thesis by A9;
    end;
    now
A14:  A*^C +^ 0 = A*^C & A*^C +^ 0 in A*^C +^ C by A2,Th27,Th32,ORDINAL1:11;
A15:  (succ A)*^C = A*^C +^ C by Th36;
      deffunc F(Ordinal) = $1*^C;
      consider fi such that
A16:  dom fi = B & for D st D in B holds fi.D = F(D) from OSLambda;
      assume for D holds B <> succ D;
      then
A17:  B is limit_ordinal by ORDINAL1:29;
      then
A18:  succ A in B by A6,ORDINAL1:28;
      then fi.(succ A) = (succ A)*^C by A16;
      then (succ A)*^C in rng fi by A16,A18,FUNCT_1:def 3;
      then
A19:  (succ A)*^C c= union sup rng fi by Th19,ZFMISC_1:74;
      B*^C = union sup fi by A6,A17,A16,Th37
        .= union sup rng fi;
      hence thesis by A19,A14,A15;
    end;
    hence thesis by A7;
  end;
  for B holds P[B] from ORDINAL1:sch 2(A4);
  hence thesis;
end;

theorem
  A c= B implies A*^C c= B*^C
proof
  assume
A1: A c= B;
A2: now
    assume
A3: C <> 0;
    now
      assume A <> B;
      then A c< B by A1;
      then A*^C in B*^C by A3,Th40,ORDINAL1:11;
      hence thesis by ORDINAL1:def 2;
    end;
    hence thesis;
  end;
  C = 0 implies thesis by Th38;
  hence thesis by A2;
end;

theorem
  A c= B implies C*^A c= C*^B
proof
  assume
A1: A c= B;
  now
    defpred P[Ordinal] means $1*^A c= $1*^B;
    assume
A2: B <> 0;
A3: for C st for D st D in C holds P[D] holds P[C]
    proof
      let C such that
A4:   for D st D in C holds D*^A c= D*^B;
A5:   now
        given D such that
A6:     C = succ D;
        D*^A c= D*^B by A4,A6,ORDINAL1:6;
        then
A7:     D*^A +^ A c= D*^B +^ A by Th34;
A8:     C*^A = D*^A +^ A & C*^B = D*^B +^ B by A6,Th36;
        D*^B +^ A c= D*^B +^ B by A1,Th33;
        hence thesis by A7,A8,XBOOLE_1:1;
      end;
A9:   now
        deffunc F(Ordinal) = $1*^A;
        assume that
A10:    C <> 0 and
A11:    for D holds C <> succ D;
        consider fi such that
A12:    dom fi = C & for D st D in C holds fi.D = F(D) from OSLambda;
        now
          let D;
          assume D in rng fi;
          then consider x being object such that
A13:      x in dom fi and
A14:      D = fi.x by FUNCT_1:def 3;
          reconsider x as Ordinal by A13;
A15:      x*^B in C*^B by A2,A12,A13,Th40;
          D = x*^A & x*^A c= x*^B by A4,A12,A13,A14;
          hence D in C*^B by A15,ORDINAL1:12;
        end;
        then
A16:    sup rng fi c= C*^B by Th20;
        C is limit_ordinal by A11,ORDINAL1:29;
        then
A17:    C*^A = union sup fi by A10,A12,Th37
          .= union sup rng fi;
        union sup rng fi c= sup rng fi by Th5;
        hence thesis by A17,A16,XBOOLE_1:1;
      end;
      now
        assume C = 0;
        then C*^A = 0 by Th35;
        hence thesis;
      end;
      hence thesis by A5,A9;
    end;
    for C holds P[C] from ORDINAL1:sch 2(A3);
    hence thesis;
  end;
  hence thesis by A1;
end;

theorem Th43:
  exp(A,0) = 1
proof
  deffunc D(Ordinal,Ordinal-Sequence) = lim $2;
  deffunc F(Ordinal) = exp(A,$1);
  deffunc C(Ordinal,Ordinal) = A*^$2;
A1: for B,C holds C = F(B) iff ex fi st C = last fi & dom fi = succ B & fi.
  0 = 1 & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C
  in succ B & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by Def16;
  thus F(0) = 1 from OSResult0(A1);
end;

theorem Th44:
  exp(A,succ B) = A*^exp(A,B)
proof
  deffunc D(Ordinal,Ordinal-Sequence) = lim $2;
  deffunc F(Ordinal) = exp(A,$1);
  deffunc C(Ordinal,Ordinal) = A *^ $2;
A1: for B,C holds C = F(B) iff ex fi st C = last fi & dom fi = succ B & fi.
  0 = 1 & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C
  in succ B & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by Def16;
  for B holds F(succ B) = C(B,F(B)) from OSResultS(A1);
  hence thesis;
end;

theorem Th45:
  B <> 0 & B is limit_ordinal implies for fi st dom fi = B & for
  C st C in B holds fi.C = exp(A,C) holds exp(A,B) = lim fi
proof
  deffunc D(Ordinal,Ordinal-Sequence) = lim $2;
  assume
A1: B <> 0 & B is limit_ordinal;
  deffunc C(Ordinal,Ordinal) = A*^$2;
  deffunc F(Ordinal) = exp(A,$1);
  let fi such that
A2: dom fi = B and
A3: for C st C in B holds fi.C = F(C);
A4: for B,C holds C = F(B) iff ex fi st C = last fi & dom fi = succ B & fi.
  0 = 1 & (for C st succ C in succ B holds fi.succ C = C(C,fi.C)) & for C st C
  in succ B & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) by Def16;
  thus F(B) = D(B,fi) from OSResultL(A4,A1,A2,A3);
end;

theorem
  exp(A,1) = A & exp(1,A) = 1
proof
  defpred P[Ordinal] means exp(1,$1) = 1;
A1: for A st P[A] holds P[succ A]
  proof
    let A;
    assume exp(1,A) = 1;
    hence exp(1,succ A) = 1*^1 by Th44
      .= 1 by Th39;
  end;
  thus exp(A,1) = A*^exp(A,0) by Lm1,Th44
    .= A*^1 by Th43
    .= A by Th39;
A2: for A st A <> 0 & A is limit_ordinal & for B st B in A holds P[B] holds
  P[A]
  proof
    deffunc F(Ordinal) = exp(1,$1);
    let A such that
A3: A <> 0 and
A4: A is limit_ordinal and
A5: for B st B in A holds exp(1,B) = 1;
    consider fi such that
A6: dom fi = A & for B st B in A holds fi.B = F(B) from OSLambda;
A7: rng fi c= { 1 }
    proof
      let x be object;
      assume x in rng fi;
      then consider y being object such that
A8:   y in dom fi and
A9:   x = fi.y by FUNCT_1:def 3;
      reconsider y as Ordinal by A8;
      x = exp(1,y) by A6,A8,A9
        .= 1 by A5,A6,A8;
      hence thesis by TARSKI:def 1;
    end;
    now
      set x = the Element of A;
      thus 0 <> 1;
      let B,C such that
A10:  B in 1 & 1 in C;
      reconsider x as Ordinal;
      take D = x;
      thus D in dom fi by A3,A6;
      let E be Ordinal;
      assume that
      D c= E and
A11:  E in dom fi;
      fi.E in rng fi by A11,FUNCT_1:def 3;
      hence B in fi.E & fi.E in C by A7,A10,TARSKI:def 1;
    end;
    then
A12: 1 is_limes_of fi by Def9;
    exp(1,A) = lim fi by A3,A4,A6,Th45;
    hence thesis by A12,Def10;
  end;
A13: P[0] by Th43;
  for A holds P[A] from OrdinalInd(A13,A1,A2);
  hence thesis;
end;

theorem
  for A ex B,C st B is limit_ordinal & C is natural & A = B +^ C
proof
  defpred Th[Ordinal] means ex B,C st B is limit_ordinal & C is natural & $1 =
  B +^ C;
A1: for A st for B st B in A holds Th[B] holds Th[A]
  proof
    let A such that
A2: for B st B in A holds Th[B];
A3: (ex B st A = succ B) implies Th[A]
    proof
      given B such that
A4:   A = succ B;
      consider C,D such that
A5:   C is limit_ordinal and
A6:   D is natural and
A7:   B = C +^ D by A2,A4,ORDINAL1:6;
      take C, E = succ D;
      thus C is limit_ordinal by A5;
      thus E in omega by A6,ORDINAL1:def 12;
      thus thesis by A4,A7,Th28;
    end;
    (for B holds A <> succ B) implies Th[A]
    proof
      assume
A8:   for D holds A <> succ D;
      take B = A, C = 0;
      thus B is limit_ordinal by A8,ORDINAL1:29;
      thus C in omega by ORDINAL1:def 11;
      thus thesis by Th27;
    end;
    hence thesis by A3;
  end;
  thus for A holds Th[A] from ORDINAL1:sch 2(A1);
end;

:: 2005.05.04, A.T.

registration
  let X be set, o be Ordinal;
  cluster X --> o -> Ordinal-yielding;
  coherence
  proof
    rng(X --> o) c= {o} & {o} c= succ o by FUNCOP_1:13,XBOOLE_1:7;
    then rng(X --> o) c= succ o;
    hence thesis;
  end;
end;

registration
  let O be Ordinal, x be object;
  cluster O --> x -> Sequence-like;
  coherence by FUNCOP_1:13;
end;

:: from ZFREFLE1, 2007.03.14, A.T.

definition
  let A,B be Ordinal;
  pred A is_cofinal_with B means
  ex xi being Ordinal-Sequence st dom xi = B &
  rng xi c= A & xi is increasing & A = sup xi;
  reflexivity
  proof
    let A;
A1: dom id A = A by RELAT_1:45;
    then reconsider xi = id A as Sequence by ORDINAL1:def 7;
A2: rng id A = A by RELAT_1:45;
    then reconsider xi as Ordinal-Sequence by Def4;
    take xi;
    thus dom xi = A & rng xi c= A by RELAT_1:45;
    thus xi is increasing
    proof
      let B,C;
      assume that
A3:   B in C and
A4:   C in dom xi;
      xi.C = C by A1,A4,FUNCT_1:18;
      hence thesis by A1,A3,A4,FUNCT_1:18,ORDINAL1:10;
    end;
    thus thesis by A2,Th18;
  end;
end;

reserve e,u for set;

theorem Th48:
  e in rng psi implies e is Ordinal
proof
  assume e in rng psi;
  then ex u being object st u in dom psi & e = psi.u by FUNCT_1:def 3;
  hence thesis;
end;

theorem
  rng psi c= sup psi
proof
  let e be object;
  assume
A1: e in rng psi;
  then e is Ordinal by Th48;
  hence thesis by A1,Th19;
end;

theorem
  A is_cofinal_with 0 implies A = 0
proof
  given psi such that
A1: dom psi = 0 and
  rng psi c= A and
  psi is increasing and
A2: A = sup psi;
  thus A = sup 0 by A1,A2,RELAT_1:42
    .= 0 by Th18;
end;

:: from ARYTM_3, 2007.10.23, A.T.

scheme
  OmegaInd {a()-> Nat, P[object]}:
   P[a()]
provided
A1: P[0] and
A2: for a being Nat st P[a] holds P[succ a]
proof
  defpred P[Ordinal] means $1 is natural implies P[$1];
A3: now
    let A;
    assume
A4: P[A];
    now
      assume succ A is natural;
      then
A5:   succ A in omega;
      A in succ A by ORDINAL1:6;
      then A is Element of omega by A5,ORDINAL1:10;
      hence P[succ A] by A2,A4;
    end;
    hence P[succ A];
  end;
A6: now
    let A;
    assume
A7: A <> 0;
    0 c= A;
    then 0 c< A by A7;
    then
A8: 0 in A by ORDINAL1:11;
A9: not A in A;
    assume A is limit_ordinal;
    then omega c= A by A8,ORDINAL1:def 11;
    then not A in omega by A9;
    hence (for B st B in A holds P[B]) implies P[A] by ORDINAL1:def 12;
  end;
A10: P[0] by A1;
  for A holds P[A] from OrdinalInd(A10,A3,A6);
  hence thesis;
end;

registration
  let a, b be Nat;
  cluster a +^ b -> natural;
  coherence
  proof
    defpred P[Nat] means a+^$1 is natural;
A1: now
      let b be Nat;
      assume P[b];
      then reconsider c = a+^b as Nat;
      a+^succ b = succ c by Th28;
      hence P[succ b];
    end;
A2: P[0] by Th27;
    thus P[b] from OmegaInd(A2,A1);
  end;
end;

:: from AMI_2, 2008.02.14, A.T.

registration
  let x,y be set, a,b be Nat;
  cluster IFEQ(x,y,a,b) -> natural;
  coherence
  proof
    per cases;
    suppose
      x = y;
      hence thesis by FUNCOP_1:def 8;
    end;
    suppose
      x <> y;
      hence thesis by FUNCOP_1:def 8;
    end;
  end;
end;

:: 2010.03.16, A.T.

scheme LambdaRecEx{A() -> set,G(set,set) -> set}:
   ex f being Function st dom f = omega & f.0 = A() &
    for n being Nat holds f.succ n = G(n,f.n)
 proof
  deffunc D(set,set) = 0;
  consider L being Sequence such that
A1: dom L = omega and
A2: 0 in omega implies L.0 = A() and
A3: for A being Ordinal st succ A in omega holds L.(succ A) = G(A,L.A) and
  for A being Ordinal st A in omega & A <> 0 & A is limit_ordinal holds L.A
  = D(A,L|A) from TSExist1;
  take L;
  thus dom L = omega by A1;
   0 in omega by ORDINAL1:def 12;
  hence L.0 = A() by A2;
  let n be Nat;
  succ n in omega by ORDINAL1:def 12;
  hence thesis by A3;
end;

reserve n for Nat;

scheme RecUn{A() -> set, F, G() -> Function, P[set,set,set]}:
 F() = G()
provided
A1: dom F() = omega and
A2: F().0 = A() and
A3: for n holds P[n,F().n,F().(succ n)] and
A4: dom G() = omega and
A5: G().0 = A() and
A6: for n holds P[n,G().n,G().(succ n)] and
A7: for n for x,y1,y2 being set st P[n,x,y1] & P[n,x,y2] holds y1 = y2
proof
  defpred P[Nat] means F().$1 = G().$1;
A8: for n st P[n] holds P[succ n]
  proof
    let n;
    assume F().n = G().n;
    then
A9: P[n,F().n,G().(succ n)] by A6;
    P[n,F().n,F().(succ n)] by A3;
    hence thesis by A7,A9;
  end;
A10: P[0] by A2,A5;
  for n holds P[n] proof let n;
    thus thesis from OmegaInd(A10,A8);
   end;
  then for x being object st x in omega holds F().x = G().x;
  hence thesis by A1,A4,FUNCT_1:2;
end;

scheme LambdaRecUn{A() -> set, F(set,set) -> set, F, G() -> Function}:
   F() = G()
provided
A1: dom F() = omega and
A2: F().0 = A() and
A3: for n holds F().(succ n) = F(n,F().n) and
A4: dom G() = omega and
A5: G().0 = A() and
A6: for n holds G().(succ n) = F(n,G().n)
proof
  defpred P[Nat,set,set] means $3=F($1,$2);
A7: for n holds P[n,G().n,G().(succ n)] by A6;
A8: for n being Nat,x,y1,y2 being set st P[n,x,y1] & P[n,x,y2]
    holds y1=y2;
A9: for n holds P[n,F().n,F().(succ n)] by A3;
  thus F() = G() from RecUn(A1,A2,A9,A4,A5,A7,A8);
end;