ORDINAL3

:: Ordinal Arithmetics
::  by Grzegorz Bancerek
::
:: Received March 1, 1990
:: Copyright (c) 1990-2026 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 ORDINAL2, ORDINAL1, TARSKI, XBOOLE_0, SETFAM_1, RELAT_1, FUNCT_1,
      SUBSET_1, ORDINAL3, CARD_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, SETFAM_1,
      ORDINAL2;
 constructors SETFAM_1, ORDINAL2, XTUPLE_0;
 registrations XBOOLE_0, ORDINAL1, ORDINAL2;
 requirements SUBSET, BOOLE, NUMERALS;
 definitions ORDINAL2, ORDINAL1, TARSKI, XBOOLE_0;
 equalities ORDINAL2, ORDINAL1;
 expansions ORDINAL2, ORDINAL1, TARSKI, XBOOLE_0;
 theorems TARSKI, FUNCT_1, ORDINAL1, SETFAM_1, ORDINAL2, XBOOLE_1, ZFMISC_1;
 schemes ORDINAL1, ORDINAL2, XBOOLE_0;

begin

reserve fi,psi for Ordinal-Sequence,
  A,A1,B,C,D for Ordinal,
  X,Y for set,
  x,y for object;

theorem
  X c= succ X by XBOOLE_1:7;

theorem
  succ X c= Y implies X c= Y
proof
  X c= succ X by XBOOLE_1:7;
  hence thesis;
end;

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

theorem
  X c= A implies union X is epsilon-transitive epsilon-connected set
proof
  assume X c= A;
  then for x st x in X holds x is Ordinal;
  hence thesis by ORDINAL1:23;
end;

theorem Th5:
  union On X is epsilon-transitive epsilon-connected set
proof
  x in On X implies x is Ordinal by ORDINAL1:def 9;
  hence thesis by ORDINAL1:23;
end;

theorem Th6:
  X c= A implies On X = X
proof
  defpred P[object] means $1 in X & $1 is Ordinal;
  assume X c= A;
  then
A1: for x being object holds x in X iff P[x];
A2: for x being object holds x in On X iff P[x] by ORDINAL1:def 9;
  thus thesis from XBOOLE_0:sch 2(A2,A1);
end;

theorem Th7:
  On {A} = {A}
proof
  {A} c= succ A by XBOOLE_1:7;
  hence thesis by Th6;
end;

theorem Th8:
  A <> {} implies {} in A
proof
A1: {} c= A;
  assume A <> {};
  then {} c< A by A1;
  hence thesis by ORDINAL1:11;
end;

theorem
  inf A = {}
proof
A1: inf A = meet A by ORDINAL2:8;
  then A <> {} implies thesis by Th8,SETFAM_1:4;
  hence thesis by A1,SETFAM_1:def 1;
end;

theorem
  inf {A} = A
proof
  thus inf {A} = meet {A} by Th7
    .= A by SETFAM_1:10;
end;

theorem
  X c= A implies meet X is Ordinal
proof
  assume X c= A;
  then inf X = meet X by Th6;
  hence thesis;
end;

registration
  let A,B;
  cluster A \/ B -> ordinal;
  coherence
  proof
    A c= B or B c= A;
    hence thesis by XBOOLE_1:12;
  end;
  cluster A /\ B -> ordinal;
  coherence
  proof
    A c= B or B c= A;
    hence thesis by XBOOLE_1:28;
  end;
end;

theorem
  A \/ B = A or A \/ B = B
proof
  A c= B or B c= A;
  hence thesis by XBOOLE_1:12;
end;

theorem
  A /\ B = A or A /\ B = B
proof
  A c= B or B c= A;
  hence thesis by XBOOLE_1:28;
end;

Lm1: 1 = succ 0;

theorem Th14:
  A in 1 implies A = {}
proof
  assume A in 1;
  hence A c= {} & {} c= A by Lm1,ORDINAL1:22;
end;

theorem
  1 = {{}} by Lm1;

theorem Th16:
  A c= 1 implies A = {} or A = 1
proof
  assume that
A1: A c= 1 and
A2: A <> {} and
A3: A <> 1;
  A c< 1 by A1,A3;
  hence contradiction by A2,Th14,ORDINAL1:11;
end;

theorem
  (A c= B or A in B) & C in D implies A+^C in B+^D
proof
  assume that
A1: A c= B or A in B and
A2: C in D;
A3: B+^C in B+^D by A2,ORDINAL2:32;
  A c= B by A1,ORDINAL1:def 2;
  hence thesis by A3,ORDINAL1:12,ORDINAL2:34;
end;

theorem
  A c= B & C c= D implies A+^C c= B+^D
proof
  assume that
A1: A c= B and
A2: C c= D;
A3: B+^C c= B+^D by A2,ORDINAL2:33;
  A+^C c= B+^C by A1,ORDINAL2:34;
  hence thesis by A3;
end;

theorem Th19:
  A in B & (C c= D & D <> {} or C in D) implies A*^C in B*^D
proof
  assume that
A1: A in B and
A2: C c= D & D <> {} or C in D;
A3: C c= D by A2,ORDINAL1:def 2;
  A*^D in B*^D by A1,A2,ORDINAL2:40;
  hence thesis by A3,ORDINAL1:12,ORDINAL2:42;
end;

theorem
  A c= B & C c= D implies A*^C c= B*^D
proof
  assume that
A1: A c= B and
A2: C c= D;
A3: B*^C c= B*^D by A2,ORDINAL2:42;
  A*^C c= B*^C by A1,ORDINAL2:41;
  hence thesis by A3;
end;

theorem Th21:
  B+^C = B+^D implies C = D
proof
  assume that
A1: B+^C = B+^D and
A2: C <> D;
  C in D or D in C by A2,ORDINAL1:14;
  then B+^C in B+^C by A1,ORDINAL2:32;
  hence contradiction;
end;

theorem Th22:
  B+^C in B+^D implies C in D
proof
  assume that
A1: B+^C in B+^D and
A2: not C in D;
  D c= C by A2,ORDINAL1:16;
  hence contradiction by A1,ORDINAL1:5,ORDINAL2:33;
end;

theorem Th23:
  B+^C c= B+^D implies C c= D
proof
  assume
A1: B+^C c= B+^D;
  B+^C c= B+^D & B+^C <> B+^D iff B+^C c< B+^D;
  then C = D or C in D by A1,Th21,Th22,ORDINAL1:11;
  hence thesis by ORDINAL1:def 2;
end;

theorem Th24:
  A c= A+^B & B c= A+^B
proof
A1: {}+^B c= A+^B by ORDINAL2:34,XBOOLE_1:2;
  A+^{} c= A+^B by ORDINAL2:33,XBOOLE_1:2;
  hence thesis by A1,ORDINAL2:27,30;
end;

theorem
  A in B implies A in B+^C & A in C+^B
proof
  assume
A1: A in B;
A2: B c= C+^B by Th24;
  B c= B+^C by Th24;
  hence thesis by A1,A2;
end;

theorem Th26:
  A+^B = {} implies A = {} & B = {} by Th24,XBOOLE_1:3;

theorem Th27:
  A c= B implies ex C st B = A+^C
proof
  defpred P[Ordinal] means A c= $1 implies ex C st $1 = A+^C;
A1: for B st P[B] holds P[succ B]
  proof
    let B such that
A2: A c= B implies ex C st B = A+^C and
A3: A c= succ B;
A4: now
      assume A <> succ B;
      then A c< succ B by A3;
      then A in succ B by ORDINAL1:11;
      then consider C such that
A5:   B = A+^C by A2,ORDINAL1:22;
      succ B = A+^succ C by A5,ORDINAL2:28;
      hence thesis;
    end;
    A = succ B implies succ B = A+^{} by ORDINAL2:27;
    hence thesis by A4;
  end;
A6: for B st B <> 0 & B is limit_ordinal & for C st C in B holds P[C]
  holds P[B]
  proof
    deffunc F(Ordinal) = A +^ $1;
    let B such that
    B <> 0 and
A7: B is limit_ordinal and
    for C st C in B holds A c= C implies ex D st C = A+^D and
A8: A c= B;
    defpred P[Ordinal] means B c= A+^$1;
A9: B = {}+^B by ORDINAL2:30;
    {}+^B c= A+^B by ORDINAL2:34,XBOOLE_1:2;
    then
A10: ex C st P[C] by A9;
    consider C such that
A11: P[C] & for D st P[D] holds C c= D from ORDINAL1:sch 1(A10);
    consider L being Ordinal-Sequence such that
A12: dom L = C & for D st D in C holds L.D = F(D) from ORDINAL2:sch 3;
A13: now
      for D st D in rng L holds D in B
      proof
        let D;
        assume D in rng L;
        then consider y being object such that
A14:    y in dom L and
A15:    D = L.y by FUNCT_1:def 3;
        reconsider y as Ordinal by A14;
A16:    not C c= y by A12,A14,ORDINAL1:5;
        L.y = A+^y by A12,A14;
        hence thesis by A11,A15,A16,ORDINAL1:16;
      end;
      then
A17:  sup rng L c= B by ORDINAL2:20;
A18:  C is limit_ordinal
      proof
        assume not thesis;
        then consider D such that
A19:    C = succ D by ORDINAL1:29;
        not C c= D by A19,ORDINAL1:5,6;
        then A+^D in B by A11,ORDINAL1:16;
        then
A20:    succ(A+^D) c= B by ORDINAL1:21;
        succ(A+^D) = A+^succ D by ORDINAL2:28;
        then B = succ(A+^D) by A11,A19,A20;
        hence contradiction by A7,ORDINAL1:29;
      end;
      assume C <> {};
      then A+^C = sup L by A12,A18,ORDINAL2:29
        .= sup rng L;
      then B = A+^C by A11,A17;
      hence thesis;
    end;
    C = {} implies B = A+^{} by A8,A11,ORDINAL2:27;
    hence thesis by A13;
  end;
A21: P[0]
  proof
    assume A c= 0;
    then A = {} by XBOOLE_1:3;
    then {} = A+^{} by ORDINAL2:30;
    hence thesis;
  end;
  for B holds P[B] from ORDINAL2:sch 1(A21,A1,A6);
  hence thesis;
end;

theorem Th28:
  A in B implies ex C st B = A+^C & C <> {}
proof
  assume
A1: A in B;
  then A c= B by ORDINAL1:def 2;
  then consider C such that
A2: B = A+^C by Th27;
  take C;
  thus B = A+^C by A2;
  assume C = {};
  then B = A by A2,ORDINAL2:27;
  hence contradiction by A1;
end;

theorem Th29:
  A <> {} & A is limit_ordinal implies B+^A is limit_ordinal
proof
  assume that
A1: A <> {} and
A2: A is limit_ordinal;
  {} c= A;
  then
A3: {} c< A by A1;
  deffunc F(Ordinal) = B +^ $1;
  consider L being Ordinal-Sequence such that
A4: dom L = A & for C st C in A holds L.C = F(C) from ORDINAL2:sch 3;
A5: B+^A = sup L by A1,A2,A4,ORDINAL2:29
    .= sup rng L;
  for C st C in B+^A holds succ C in B+^A
  proof
    let C such that
A6: C in B+^A;
A7: now
      assume not C in B;
      then consider D such that
A8:   C = B+^D by Th27,ORDINAL1:16;
      now
        assume not D in A;
        then B+^A c= B+^D by ORDINAL1:16,ORDINAL2:33;
        then C in C by A6,A8;
        hence contradiction;
      end;
      then
A9:   succ D in A by A2,ORDINAL1:28;
      then L.(succ D) = B+^succ D by A4
        .= succ(B+^D) by ORDINAL2:28;
      then succ C in rng L by A4,A8,A9,FUNCT_1:def 3;
      hence thesis by A5,ORDINAL2:19;
    end;
    now
      assume C in B;
      then
A10:  succ C c= B by ORDINAL1:21;
A11:  (succ C)+^{} = succ C by ORDINAL2:27;
      B+^{} in B+^A by A3,ORDINAL1:11,ORDINAL2:32;
      hence thesis by A10,A11,ORDINAL1:12,ORDINAL2:34;
    end;
    hence thesis by A7;
  end;
  hence thesis by ORDINAL1:28;
end;

theorem Th30:
  A+^B+^C = A+^(B+^C)
proof
  defpred Sigma[Ordinal] means A+^B+^$1 = A+^(B+^$1);
A1: for C st Sigma[C] holds Sigma[succ C]
  proof
    let C such that
A2: A+^B+^C = A+^(B+^C);
    thus A+^B+^succ C = succ(A+^B+^C) by ORDINAL2:28
      .= A+^succ(B+^C) by A2,ORDINAL2:28
      .= A+^(B+^succ C) by ORDINAL2:28;
  end;
A3: for C st C <> 0 & C is limit_ordinal & for D st D in C holds Sigma[D]
  holds Sigma[C]
  proof
    deffunc F(Ordinal) = A +^ B +^ $1;
    let C such that
A4: C <> 0 and
A5: C is limit_ordinal and
A6: for D st D in C holds Sigma[D];
    consider L being Ordinal-Sequence such that
A7: dom L = C & for D st D in C holds L.D = F(D) from ORDINAL2:sch 3;
    deffunc F(Ordinal) = A +^ $1;
    consider L1 being Ordinal-Sequence such that
A8: dom L1 = B+^C & for D st D in B+^C holds L1.D = F(D) from
    ORDINAL2:sch 3;
A9: rng L c= rng L1
    proof
      let x be object;
      assume x in rng L;
      then consider y being object such that
A10:  y in dom L and
A11:  x = L.y by FUNCT_1:def 3;
      reconsider y as Ordinal by A10;
A12:  B+^y in B+^C by A7,A10,ORDINAL2:32;
      L.y = A+^B+^y by A7,A10;
      then
A13:  L.y = A+^(B+^y) by A6,A7,A10;
      L1.(B+^y) = A+^(B+^y) by A7,A8,A10,ORDINAL2:32;
      hence thesis by A8,A11,A13,A12,FUNCT_1:def 3;
    end;
A14: B+^C <> {} by A4,Th26;
    B+^C is limit_ordinal by A4,A5,Th29;
    then
A15: A+^(B+^C) = sup L1 by A8,A14,ORDINAL2:29
      .= sup rng L1;
    A+^B+^C = sup L by A4,A5,A7,ORDINAL2:29
      .= sup rng L;
    hence A+^B+^C c= A+^(B+^C) by A15,A9,ORDINAL2:22;
    let x be object;
    assume
A16: x in A+^(B+^C);
    then reconsider x9 = x as Ordinal;
A17: now
A18:  A c= A+^B by Th24;
      assume
A19:  not x in A+^B;
      then A+^B c= x9 by ORDINAL1:16;
      then consider E being Ordinal such that
A20:  x9 = A+^E by A18,Th27,XBOOLE_1:1;
      B c= E by A19,A20,ORDINAL1:16,ORDINAL2:32;
      then consider F being Ordinal such that
A21:  E = B+^F by Th27;
A22:  now
        assume not F in C;
        then B+^C c= B+^F by ORDINAL1:16,ORDINAL2:33;
        then A+^(B+^C) c= A+^(B+^F) by ORDINAL2:33;
        then x9 in x9 by A16,A20,A21;
        hence contradiction;
      end;
      then x = A+^B+^F by A6,A20,A21;
      hence thesis by A22,ORDINAL2:32;
    end;
A23: A+^B+^{} = A+^B by ORDINAL2:27;
    A+^B+^{} c= A+^B+^C by ORDINAL2:33,XBOOLE_1:2;
    hence thesis by A23,A17;
  end;
  A+^B+^{} = A+^B by ORDINAL2:27
    .= A+^(B+^{}) by ORDINAL2:27;
  then
A24: Sigma[0];
  for C holds Sigma[C] from ORDINAL2:sch 1(A24,A1,A3);
  hence thesis;
end;

theorem
  A*^B = {} implies A = {} or B = {}
proof
  assume that
A1: A*^B = {} and
A2: A <> {} and
A3: B <> {};
  {} c= A;
  then {} c< A by A2;
  hence contradiction by A1,A3,ORDINAL1:11,ORDINAL2:40;
end;

theorem
  A in B & C <> {} implies A in B*^C & A in C*^B
proof
  assume that
A1: A in B and
A2: C <> {};
  {} c= C;
  then {} c< C by A2;
  then {} in C by ORDINAL1:11;
  then
A3: 1 c= C by Lm1,ORDINAL1:21;
  then
A4: 1*^B c= C*^B by ORDINAL2:41;
A5: 1*^B = B by ORDINAL2:39;
A6: B*^1 = B by ORDINAL2:39;
  B*^1 c= B*^C by A3,ORDINAL2:42;
  hence thesis by A1,A4,A6,A5;
end;

theorem Th33:
  B*^A = C*^A & A <> {} implies B = C
proof
  assume that
A1: B*^A = C*^A and
A2: A <> {} and
A3: B <> C;
  B in C or C in B by A3,ORDINAL1:14;
  then B*^A in B*^A by A1,A2,ORDINAL2:40;
  hence contradiction;
end;

theorem Th34:
  B*^A in C*^A implies B in C
proof
  assume that
A1: B*^A in C*^A and
A2: not B in C;
  C c= B by A2,ORDINAL1:16;
  hence contradiction by A1,ORDINAL1:5,ORDINAL2:41;
end;

theorem Th35:
  B*^A c= C*^A & A <> {} implies B c= C
proof
  assume
A1: B*^A c= C*^A;
  B*^A c= C*^A & B*^A <> C*^A iff B*^A c< C*^A;
  then (A <> {} implies B = C) or B in C by A1,Th33,Th34,ORDINAL1:11;
  hence thesis by ORDINAL1:def 2;
end;

theorem Th36:
  B <> {} implies A c= A*^B & A c= B*^A
proof
  assume B <> {};
  then {} in B by Th8;
  then
A1: 1 c= B by Lm1,ORDINAL1:21;
  then
A2: A*^1 c= A*^B by ORDINAL2:42;
  1*^A c= B*^A by A1,ORDINAL2:41;
  hence thesis by A2,ORDINAL2:39;
end;

theorem
  A*^B = 1 implies A = 1 & B = 1
proof
  assume
A1: A*^B = 1;
  then
A2: B <> {} by ORDINAL2:38;
  {} c= B;
  then {} c< B by A2;
  then {} in B by ORDINAL1:11;
  then
A3: 1 c= B by Lm1,ORDINAL1:21;
A4: now
A5: B = 1*^B by ORDINAL2:39;
    assume 1 in A;
    hence contradiction by A1,A2,A3,A5,ORDINAL1:5,ORDINAL2:40;
  end;
  now
    assume A in 1;
    then A c= {} by Lm1,ORDINAL1:22;
    then A = {} by XBOOLE_1:3;
    hence contradiction by A1,ORDINAL2:35;
  end;
  hence A = 1 by A4,ORDINAL1:14;
  hence thesis by A1,ORDINAL2:39;
end;

theorem Th38:
  A in B+^C implies A in B or ex D st D in C & A = B+^D
proof
  assume that
A1: A in B+^C and
A2: not A in B;
  consider D such that
A3: A = B+^D by A2,Th27,ORDINAL1:16;
  take D;
  assume not thesis;
  then C c= D by A3,ORDINAL1:16;
  hence contradiction by A1,A3,ORDINAL1:5,ORDINAL2:33;
end;

definition
  let C,fi;
  func C+^fi -> Ordinal-Sequence means
  :Def1:
  dom it = dom fi & for A st A in dom fi holds it.A = C+^(fi.A);
  existence
  proof
    deffunc F(Ordinal) = C+^(fi.$1);
    thus ex F being Ordinal-Sequence st dom F = dom fi & for A st A in dom fi
    holds F.A = F(A) from ORDINAL2:sch 3;
  end;
  uniqueness
  proof
    let f1,f2 be Ordinal-Sequence such that
A1: dom f1 = dom fi and
A2: for A st A in dom fi holds f1.A = C+^(fi.A) and
A3: dom f2 = dom fi and
A4: for A st A in dom fi holds f2.A = C+^(fi.A);
    now
      let x be object;
      assume
A5:   x in dom fi;
      then reconsider A = x as Ordinal;
      thus f1.x = C+^(fi.A) by A2,A5
        .= f2.x by A4,A5;
    end;
    hence thesis by A1,A3,FUNCT_1:2;
  end;
  func fi+^C -> Ordinal-Sequence means
  dom it = dom fi & for A st A in dom fi holds it.A = (fi.A)+^C;
  existence
  proof
    deffunc F(Ordinal) = (fi.$1)+^C;
    thus ex F being Ordinal-Sequence st dom F = dom fi & for A st A in dom fi
    holds F.A = F(A) from ORDINAL2:sch 3;
  end;
  uniqueness
  proof
    let f1,f2 be Ordinal-Sequence such that
A6: dom f1 = dom fi and
A7: for A st A in dom fi holds f1.A = (fi.A)+^C and
A8: dom f2 = dom fi and
A9: for A st A in dom fi holds f2.A = (fi.A)+^C;
    now
      let x be object;
      assume
A10:  x in dom fi;
      then reconsider A = x as Ordinal;
      thus f1.x = (fi.A)+^C by A7,A10
        .= f2.x by A9,A10;
    end;
    hence thesis by A6,A8,FUNCT_1:2;
  end;
  func C*^fi -> Ordinal-Sequence means
  dom it = dom fi & for A st A in dom fi holds it.A = C*^(fi.A);
  existence
  proof
    deffunc F(Ordinal) = C*^(fi.$1);
    thus ex F being Ordinal-Sequence st dom F = dom fi & for A st A in dom fi
    holds F.A = F(A) from ORDINAL2:sch 3;
  end;
  uniqueness
  proof
    let f1,f2 be Ordinal-Sequence such that
A11: dom f1 = dom fi and
A12: for A st A in dom fi holds f1.A = C*^(fi.A) and
A13: dom f2 = dom fi and
A14: for A st A in dom fi holds f2.A = C*^(fi.A);
    now
      let x be object;
      assume
A15:  x in dom fi;
      then reconsider A = x as Ordinal;
      thus f1.x = C*^(fi.A) by A12,A15
        .= f2.x by A14,A15;
    end;
    hence thesis by A11,A13,FUNCT_1:2;
  end;
  func fi*^C -> Ordinal-Sequence means
  : Def4:
  dom it = dom fi & for A st A in dom fi holds it.A = (fi.A)*^C;
  existence
  proof
    deffunc F(Ordinal) = (fi.$1)*^C;
    thus ex F being Ordinal-Sequence st dom F = dom fi & for A st A in dom fi
    holds F.A = F(A) from ORDINAL2:sch 3;
  end;
  uniqueness
  proof
    let f1,f2 be Ordinal-Sequence such that
A16: dom f1 = dom fi and
A17: for A st A in dom fi holds f1.A = (fi.A)*^C and
A18: dom f2 = dom fi and
A19: for A st A in dom fi holds f2.A = (fi.A)*^C;
    now
      let x be object;
      assume
A20:  x in dom fi;
      then reconsider A = x as Ordinal;
      thus f1.x = (fi.A)*^C by A17,A20
        .= f2.x by A19,A20;
    end;
    hence thesis by A16,A18,FUNCT_1:2;
  end;
end;

theorem Th39:
  {} <> dom fi & dom fi = dom psi & (for A,B st A in dom fi & B =
  fi.A holds psi.A = C+^B) implies sup psi = C+^sup fi
proof
  assume that
A1: {} <> dom fi and
A2: dom fi = dom psi and
A3: for A,B st A in dom fi & B = fi.A holds psi.A = C+^B;
  set z = the Element of dom fi;
  reconsider z9 = fi.z as Ordinal;
A4: C+^sup rng fi c= sup rng psi
  proof
    let x be object;
    assume
A5: x in C+^sup rng fi;
    then reconsider A = x as Ordinal;
A6: now
      given B such that
A7:   B in sup rng fi and
A8:   A = C+^B;
      consider D such that
A9:   D in rng fi and
A10:  B c= D by A7,ORDINAL2:21;
      consider x being object such that
A11:  x in dom fi and
A12:  D = fi.x by A9,FUNCT_1:def 3;
      reconsider x as Ordinal by A11;
      psi.x = C+^D by A3,A11,A12;
      then C+^D in rng psi by A2,A11,FUNCT_1:def 3;
      then C+^D in sup rng psi by ORDINAL2:19;
      hence A in sup rng psi by A8,A10,ORDINAL1:12,ORDINAL2:33;
    end;
    now
      C+^z9 = psi.z by A1,A3;
      then C+^z9 in rng psi by A1,A2,FUNCT_1:def 3;
      then
A13:  C+^z9 in sup rng psi by ORDINAL2:19;
      assume
A14:  A in C;
      C c= C+^z9 by Th24;
      then A c= C+^z9 by A14,ORDINAL1:def 2;
      hence A in sup rng psi by A13,ORDINAL1:12;
    end;
    hence thesis by A5,A6,Th38;
  end;
  sup rng psi c= C+^sup rng fi
  proof
    let x be object;
    assume
A15: x in sup rng psi;
    then reconsider A = x as Ordinal;
    consider B such that
A16: B in rng psi and
A17: A c= B by A15,ORDINAL2:21;
    consider y being object such that
A18: y in dom psi and
A19: B = psi.y by A16,FUNCT_1:def 3;
    reconsider y as Ordinal by A18;
    reconsider y9 = fi.y as Ordinal;
    y9 in rng fi by A2,A18,FUNCT_1:def 3;
    then
A20: y9 in sup rng fi by ORDINAL2:19;
    B = C+^y9 by A2,A3,A18,A19;
    then B in C+^sup rng fi by A20,ORDINAL2:32;
    hence thesis by A17,ORDINAL1:12;
  end;
  hence thesis by A4;
end;

theorem Th40:
  A is limit_ordinal implies A*^B is limit_ordinal
proof
A1: now
    deffunc F(Ordinal) = $1 *^ B;
    assume that
A2: A <> {} and
A3: A is limit_ordinal;
    consider fi such that
A4: dom fi = A & for C st C in A holds fi.C = F(C) from ORDINAL2:sch 3;
A5: A*^B = union sup fi by A2,A3,A4,ORDINAL2:37
      .= union sup rng fi;
    for C st C in A*^B holds succ C in A*^B
    proof
      let C;
      assume
A6:   C in A*^B;
      then consider X such that
A7:   C in X and
A8:   X in sup rng fi by A5,TARSKI:def 4;
      reconsider X as Ordinal by A8;
      consider D such that
A9:   D in rng fi and
A10:  X c= D by A8,ORDINAL2:21;
      consider x being object such that
A11:  x in dom fi and
A12:  D = fi.x by A9,FUNCT_1:def 3;
      succ C c= D by A7,A10,ORDINAL1:21;
      then
A13:  succ C in succ D by ORDINAL1:22;
      reconsider x as Ordinal by A11;
A14:  succ x in dom fi by A3,A4,A11,ORDINAL1:28;
      then fi.succ x = (succ x)*^B by A4
        .= x*^B+^B by ORDINAL2:36;
      then x*^B+^B in rng fi by A14,FUNCT_1:def 3;
      then
A15:  x*^B+^B in sup rng fi by ORDINAL2:19;
A16:  x*^B+^succ {} = succ(x*^B+^{}) by ORDINAL2:28;
      B<>{} by A6,ORDINAL2:38;
      then {} in B by Th8;
      then
A17:  succ {} c= B by ORDINAL1:21;
A18:  x*^B+^{} = x*^B by ORDINAL2:27;
      x*^B = fi.x by A4,A11;
      then succ D in sup rng fi by A12,A17,A16,A18,A15,ORDINAL1:12,ORDINAL2:33;
      hence thesis by A5,A13,TARSKI:def 4;
    end;
    hence thesis by ORDINAL1:28;
  end;
  assume A is limit_ordinal;
  hence thesis by A1,ORDINAL2:35;
end;

theorem Th41:
  A in B*^C & B is limit_ordinal implies ex D st D in B & A in D*^ C
proof
  assume that
A1: A in B*^C and
A2: B is limit_ordinal;
  deffunc F(Ordinal) = $1 *^ C;
  consider fi such that
A3: dom fi = B & for D st D in B holds fi.D = F(D) from ORDINAL2:sch 3;
  B <> {} by A1,ORDINAL2:35;
  then B*^C = union sup fi by A2,A3,ORDINAL2:37
    .= union sup rng fi;
  then consider X such that
A4: A in X and
A5: X in sup rng fi by A1,TARSKI:def 4;
  reconsider X as Ordinal by A5;
  consider D such that
A6: D in rng fi and
A7: X c= D by A5,ORDINAL2:21;
  consider x being object such that
A8: x in dom fi and
A9: D = fi.x by A6,FUNCT_1:def 3;
  reconsider x as Ordinal by A8;
  take E = succ x;
  thus E in B by A2,A3,A8,ORDINAL1:28;
A10: D+^{} = D by ORDINAL2:27;
A11: C <> {} by A1,ORDINAL2:38;
  E*^C = x*^C+^C by ORDINAL2:36
    .= D+^C by A3,A8,A9;
  then D in E*^C by A11,A10,Th8,ORDINAL2:32;
  hence thesis by A4,A7,ORDINAL1:10;
end;

theorem Th42:
  dom fi = dom psi & C <> {} & sup fi is limit_ordinal & (for A,B
  st A in dom fi & B = fi.A holds psi.A = B*^C) implies sup psi = (sup fi)*^C
proof
  assume that
A1: dom fi = dom psi and
A2: C <> {} and
A3: sup fi is limit_ordinal and
A4: for A,B st A in dom fi & B = fi.A holds psi.A = B*^C;
A5: (sup rng fi)*^C c= sup rng psi
  proof
    let x be object;
    assume
A6: x in (sup rng fi)*^C;
    then reconsider A = x as Ordinal;
    consider B such that
A7: B in sup rng fi and
A8: A in B*^C by A3,A6,Th41;
    consider D such that
A9: D in rng fi and
A10: B c= D by A7,ORDINAL2:21;
    consider y being object such that
A11: y in dom fi and
A12: D = fi.y by A9,FUNCT_1:def 3;
    reconsider y as Ordinal by A11;
    reconsider y9 = psi.y as Ordinal;
A13: y9 in rng psi by A1,A11,FUNCT_1:def 3;
    y9 = D*^C by A4,A11,A12;
    then
A14: D*^C in sup rng psi by A13,ORDINAL2:19;
    B*^C c= D*^C by A10,ORDINAL2:41;
    hence thesis by A8,A14,ORDINAL1:10;
  end;
  sup rng psi c= (sup rng fi)*^C
  proof
    let x be object;
    assume
A15: x in sup rng psi;
    then reconsider A = x as Ordinal;
    consider B such that
A16: B in rng psi and
A17: A c= B by A15,ORDINAL2:21;
    consider y being object such that
A18: y in dom psi and
A19: B = psi.y by A16,FUNCT_1:def 3;
    reconsider y as Ordinal by A18;
    reconsider y9 = fi.y as Ordinal;
    y9 in rng fi by A1,A18,FUNCT_1:def 3;
    then
A20: y9 in sup rng fi by ORDINAL2:19;
    B = y9*^C by A1,A4,A18,A19;
    then B in (sup rng fi)*^C by A2,A20,ORDINAL2:40;
    hence thesis by A17,ORDINAL1:12;
  end;
  hence thesis by A5;
end;

theorem Th43:
  {} <> dom fi implies sup (C+^fi) = C+^sup fi
proof
A1: for A,B st A in dom fi & B = fi.A holds (C+^fi).A = C+^B by Def1;
  dom (C+^fi) = dom fi by Def1;
  hence thesis by A1,Th39;
end;

theorem Th44:
  {} <> dom fi & C <> {} & sup fi is limit_ordinal implies sup (fi
  *^C) = (sup fi)*^C
proof
A1: for A,B st A in dom fi & B = fi.A holds (fi*^C).A = B*^C by Def4;
  dom (fi*^C) = dom fi by Def4;
  hence thesis by A1,Th42;
end;

theorem Th45:
  B <> {} implies union(A+^B) = A+^union B
proof
  assume
A1: B <> {};
A2: now
    assume not ex C st B = succ C;
    then
A3: B is limit_ordinal by ORDINAL1:29;
    then A+^B is limit_ordinal by A1,Th29;
    then union(A+^B) = A+^B;
    hence thesis by A3;
  end;
  now
    given C such that
A4: B = succ C;
    thus union(A+^B) = union succ (A+^C) by A4,ORDINAL2:28
      .= A+^C by ORDINAL2:2
      .= A+^union B by A4,ORDINAL2:2;
  end;
  hence thesis by A2;
end;

theorem Th46:
  (A+^B)*^C = A*^C +^ B*^C
proof
  defpred S[Ordinal] means (A+^$1)*^C = A*^C +^ $1*^C;
A1: for B st S[B] holds S[succ B]
  proof
    let B such that
A2: (A+^B)*^C = A*^C +^ B*^C;
    thus (A+^succ B)*^C = (succ(A+^B))*^C by ORDINAL2:28
      .= A*^C +^ B*^C +^ C by A2,ORDINAL2:36
      .= A*^C +^ (B*^C +^ C) by Th30
      .= A*^C +^ (succ B)*^C by ORDINAL2:36;
  end;
A3: for B st B <> 0 & B is limit_ordinal & for D st D in B holds S[D] holds
  S[B]
  proof
    deffunc F(Ordinal) = A +^ $1;
    let B such that
A4: B <> 0 and
A5: B is limit_ordinal and
A6: for D st D in B holds S[D];
    consider fi such that
A7: dom fi = B & for D st D in B holds fi.D = F(D) from ORDINAL2:sch
    3;
    A+^B is limit_ordinal by A4,A5,Th29;
    then
A8: (A+^B)*^C is limit_ordinal by Th40;
A9: dom (fi*^C) = dom fi by Def4;
A10: now
      assume
A11:  C = {};
      then
A12:  A*^C = {} by ORDINAL2:38;
A13:  B*^C = {} by A11,ORDINAL2:38;
      (A+^B)*^C = {} by A11,ORDINAL2:38;
      hence thesis by A12,A13,ORDINAL2:27;
    end;
    deffunc F(Ordinal) = $1 *^ C;
    consider psi such that
A14: dom psi = B & for D st D in B holds psi.D = F(D) from ORDINAL2:
    sch 3;
A15: now
      let x be object;
      assume
A16:  x in B;
      then reconsider k = x as Ordinal;
      reconsider m = fi.k, n = psi.k as Ordinal;
      thus (fi*^C).x = m*^C by A7,A16,Def4
        .= (A+^k)*^C by A7,A16
        .= A*^C+^k*^C by A6,A16
        .= A*^C+^n by A14,A16
        .= (A*^C+^psi).x by A14,A16,Def1;
    end;
    reconsider k = psi.{} as Ordinal;
    {} in B by A4,Th8;
    then k in rng psi by A14,FUNCT_1:def 3;
    then
A17: k in sup rng psi by ORDINAL2:19;
    dom (A*^C+^psi) = dom psi by Def1;
    then
A18: fi*^C = A*^C+^psi by A7,A14,A9,A15,FUNCT_1:2;
A19: A+^B = sup fi by A4,A5,A7,ORDINAL2:29;
    now
      assume C <> {};
      then (A+^B)*^C = sup(fi*^C) by A4,A5,A7,A19,Th29,Th44
        .= A*^C+^sup psi by A4,A14,A18,Th43;
      hence (A+^B)*^C = union(A*^C+^sup psi) by A8
        .= A*^C+^union sup psi by A17,Th45
        .= A*^C+^B*^C by A4,A5,A14,ORDINAL2:37;
    end;
    hence thesis by A10;
  end;
  (A+^{})*^C = A*^C by ORDINAL2:27
    .= A*^C +^ {} by ORDINAL2:27
    .= A*^C +^ {}*^C by ORDINAL2:35;
  then
A20: S[0];
  for B holds S[B] from ORDINAL2:sch 1(A20,A1,A3);
  hence thesis;
end;

theorem Th47:
  A <> {} implies ex C,D st B = C*^A+^D & D in A
proof
  defpred I[Ordinal] means ex C,D st $1 = C*^A+^D & D in A;
  assume
A1: A <> {};
A2: for B st B <> 0 & B is limit_ordinal & for A1 st A1 in B holds I[A1]
  holds I[B]
  proof
    {} in A by A1,Th8;
    then
A3: succ 0 c= A by ORDINAL1:21;
    let B such that
    B <> 0 and
A4: B is limit_ordinal and
    for A1 st A1 in B holds I[A1];
    defpred P[Ordinal] means $1 in B & B in $1*^A;
    B*^1 = B by ORDINAL2:39;
    then
A5: B c= B*^A by A3,ORDINAL2:42;
A6: now
      assume B <> B*^A;
      then B c< B*^A by A5;
      then B in B*^A by ORDINAL1:11;
      then
A7:   ex C st P[C] by A4,Th41;
      consider C such that
A8:   P[C] and
A9:   for C1 being Ordinal st P[C1] holds C c= C1 from ORDINAL1:sch 1
      (A7);
      now
        assume C is limit_ordinal;
        then consider C1 being Ordinal such that
A10:    C1 in C and
A11:    B in C1*^A by A8,Th41;
        C1 in B by A8,A10,ORDINAL1:10;
        hence contradiction by A9,A10,A11,ORDINAL1:5;
      end;
      then consider C1 being Ordinal such that
A12:  C = succ C1 by ORDINAL1:29;
A13:  C1 in C by A12,ORDINAL1:6;
      then C1 in B by A8,ORDINAL1:10;
      then not B in C1*^A by A9,A13,ORDINAL1:5;
      then consider D such that
A14:  B = C1*^A+^D by Th27,ORDINAL1:16;
      thus I[B]
      proof
        take C1,D;
        thus B = C1*^A+^D by A14;
        C1*^A+^D in C1*^A+^A by A8,A12,A14,ORDINAL2:36;
        hence thesis by Th22;
      end;
    end;
    B = B*^A implies B = B*^A+^{} & {} in A by A1,Th8,ORDINAL2:27;
    hence thesis by A6;
  end;
A15: for B st I[B] holds I[succ B]
  proof
    let B;
    given C,D such that
A16: B = C*^A+^D and
A17: D in A;
A18: now
      assume not succ D in A;
      then
A19:  A c= succ D by ORDINAL1:16;
      take C1 = succ C, D1 = {};
      succ D c= A by A17,ORDINAL1:21;
      then
A20:  A = succ D by A19;
      thus C1*^A+^D1 = C1*^A by ORDINAL2:27
        .= C*^A+^A by ORDINAL2:36
        .= succ B by A16,A20,ORDINAL2:28;
      thus D1 in A by A1,Th8;
    end;
    now
      assume
A21:  succ D in A;
      take C1 = C, D1 = succ D;
      thus C1*^A+^D1 = succ B by A16,ORDINAL2:28;
      thus D1 in A by A21;
    end;
    hence thesis by A18;
  end;
A22: I[0]
  proof
    take C = {}, D = {};
    thus 0 = {}+^{} by ORDINAL2:27
      .= C*^A+^D by ORDINAL2:35;
    thus thesis by A1,Th8;
  end;
  for B holds I[B] from ORDINAL2:sch 1(A22,A15,A2);
  hence thesis;
end;

theorem Th48:
  for C1,D1,C2,D2 being Ordinal st C1*^A+^D1 = C2*^A+^D2 & D1 in A
  & D2 in A holds C1 = C2 & D1 = D2
proof
  let C1,D1,C2,D2 be Ordinal such that
A1: C1*^A+^D1 = C2*^A+^D2 and
A2: D1 in A and
A3: D2 in A;
  set B = C1*^A+^D1;
A4: now
    assume C2 in C1;
    then consider C such that
A5: C1 = C2+^C and
A6: C <> {} by Th28;
    B = C2*^A+^C*^A+^D1 by A5,Th46
      .= C2*^A+^(C*^A+^D1) by Th30;
    then
A7: D2 = C*^A+^D1 by A1,Th21;
A8: C*^A c= C*^A+^D1 by Th24;
    A c= C*^A by A6,Th36;
    hence contradiction by A3,A7,A8,ORDINAL1:5;
  end;
  now
    assume C1 in C2;
    then consider C such that
A9: C2 = C1+^C and
A10: C <> {} by Th28;
    B = C1*^A+^C*^A+^D2 by A1,A9,Th46
      .= C1*^A+^(C*^A+^D2) by Th30;
    then
A11: D1 = C*^A+^D2 by Th21;
A12: C*^A c= C*^A+^D2 by Th24;
    A c= C*^A by A10,Th36;
    hence contradiction by A2,A11,A12,ORDINAL1:5;
  end;
  hence C1 = C2 by A4,ORDINAL1:14;
  hence thesis by A1,Th21;
end;

theorem Th49:
  1 in B & A <> {} & A is limit_ordinal implies for fi st dom fi =
  A & for C st C in A holds fi.C = C*^B holds A*^B = sup fi
proof
  assume that
A1: 1 in B and
A2: A <> {} and
A3: A is limit_ordinal;
  let fi;
  assume that
A4: dom fi = A and
A5: for C st C in A holds fi.C = C*^B;
  now
    given C such that
A6: sup fi = succ C;
    consider D such that
A7: D in rng fi and
A8: C c= D by A6,ORDINAL1:6,ORDINAL2:21;
    D in sup fi by A7,ORDINAL2:19;
    then
A9: succ D c= succ C by A6,ORDINAL1:21;
    succ C c= succ D by A8,ORDINAL2:1;
    then succ C = succ D by A9;
    then C = D by ORDINAL1:7;
    then consider x being object such that
A10: x in dom fi and
A11: C = fi.x by A7,FUNCT_1:def 3;
    reconsider x as Ordinal by A10;
A12: C = x*^B by A4,A5,A10,A11;
    C+^1 in C+^B by A1,ORDINAL2:32;
    then
A13: sup fi in C+^B by A6,ORDINAL2:31;
A14: (succ x)*^B = x*^B+^B by ORDINAL2:36;
A15: succ x in dom fi by A3,A4,A10,ORDINAL1:28;
    then fi.succ x = (succ x)*^B by A4,A5;
    then C+^B in rng fi by A15,A12,A14,FUNCT_1:def 3;
    hence contradiction by A13,ORDINAL2:19;
  end;
  then
A16: sup fi is limit_ordinal by ORDINAL1:29;
  A*^B = union sup fi by A2,A3,A4,A5,ORDINAL2:37;
  hence thesis by A16;
end;

theorem
  (A*^B)*^C = A*^(B*^C)
proof
  defpred P[Ordinal] means ($1*^B)*^C = $1*^(B*^C);
A1: {}*^C = {} by ORDINAL2:35;
A2: for A st P[A] holds P[succ A]
  proof
    let A such that
A3: (A*^B)*^C = A*^(B*^C);
    thus ((succ A)*^B)*^C = (A*^B+^B)*^C by ORDINAL2:36
      .= A*^(B*^C)+^B*^C by A3,Th46
      .= A*^(B*^C)+^1*^(B*^C) by ORDINAL2:39
      .= (A+^1)*^(B*^C) by Th46
      .= (succ A)*^(B*^C) by ORDINAL2:31;
  end;
A4: for A st A <> 0 & A is limit_ordinal & for D st D in A holds P[D] holds
  P[A]
  proof
    let A such that
A5: A <> 0 and
A6: A is limit_ordinal and
A7: for D st D in A holds (D*^B)*^C = D*^(B*^C);
A8: now
      deffunc F(Ordinal) = $1 *^ B;
      assume that
A9:   1 in B and
A10:  1 in C;
      consider fi such that
A11:  dom fi = A & for D st D in A holds fi.D = F(D) from ORDINAL2:
      sch 3;
A12:  dom(fi*^C) = A & for D st D in A holds (fi*^C).D = D*^(B*^C)
      proof
        thus dom(fi*^C) = A by A11,Def4;
        let D;
        assume
A13:    D in A;
        then
A14:    fi.D = D*^B by A11;
        (fi*^C).D = (fi.D)*^C by A11,A13,Def4;
        hence thesis by A7,A13,A14;
      end;
      1 = 1*^1 by ORDINAL2:39;
      then 1 in B*^C by A9,A10,Th19;
      then
A15:  A*^(B*^C) = sup(fi*^C) by A5,A6,A12,Th49;
      A*^B = sup fi by A5,A6,A9,A11,Th49;
      hence thesis by A5,A6,A10,A11,A15,Th40,Th44;
    end;
    now
      assume not (1 in B & 1 in C);
      then
A16:  B = {} or B = 1 or C = {} or C = 1 by Th16,ORDINAL1:16;
A17:  {}*^C = {} by ORDINAL2:35;
A18:  A*^B*^1 = A*^B by ORDINAL2:39;
A19:  (A*^B)*^{} = {} by ORDINAL2:38;
A20:  A*^1 = A by ORDINAL2:39;
      A*^{} = {} by ORDINAL2:38;
      hence thesis by A16,A17,A20,A19,A18,ORDINAL2:38,39;
    end;
    hence thesis by A8;
  end;
  {}*^B = {} by ORDINAL2:35;
  then
A21: P[0] by A1,ORDINAL2:35;
  for A holds P[A] from ORDINAL2:sch 1(A21,A2,A4);
  hence thesis;
end;

definition
  let A,B;
  func A -^ B -> Ordinal means
  :Def5:
  A = B+^it if B c= A otherwise it = {};
  existence by Th27;
  uniqueness by Th21;
  consistency;
  func A div^ B -> Ordinal means
  :Def6:
  ex C st A = it*^B+^C & C in B if B <> {} otherwise it = {};
  consistency;
  existence by Th47;
  uniqueness by Th48;
end;

definition
  let A,B;
  func A mod^ B -> Ordinal equals
  A-^(A div^ B)*^B;
  correctness;
end;

theorem
  A in B implies B = A+^(B-^A)
proof
  assume A in B;
  then A c= B by ORDINAL1:def 2;
  hence thesis by Def5;
end;

theorem Th52:
  A+^B-^A = B
proof
  A c= A+^B by Th24;
  hence thesis by Def5;
end;

theorem Th53:
  A in B & (C c= A or C in A) implies A-^C in B-^C
proof
  assume that
A1: A in B and
A2: C c= A or C in A;
  A c= B by A1,ORDINAL1:def 2;
  then C c= B by A2,ORDINAL1:def 2;
  then
A3: B = C+^(B-^C) by Def5;
  C c= A by A2,ORDINAL1:def 2;
  then A = C+^(A-^C) by Def5;
  hence thesis by A1,A3,Th22;
end;

theorem Th54:
  A-^A = {}
proof
  A+^{} = A by ORDINAL2:27;
  hence thesis by Def5;
end;

theorem
  A in B implies B-^A <> {} & {} in B-^A
proof
  assume A in B;
  then A-^A in B-^A by Th53;
  hence thesis by Th54;
end;

theorem Th56:
  A-^{} = A & {}-^A = {}
proof
A1: {}+^A = A by ORDINAL2:30;
  {} c= A;
  hence A-^{} = A by A1,Def5;
  not A c= {} or A c= {};
  then thesis or A = {} by Def5,XBOOLE_1:3;
  hence thesis by A1,Def5;
end;

theorem
  A-^(B+^C) = (A-^B)-^C
proof
  now
    per cases;
    suppose
      B+^C c= A;
      then A = B+^C+^(A-^(B+^C)) by Def5;
      then A = B+^(C+^(A-^(B+^C))) by Th30;
      then C+^(A-^(B+^C)) = A-^B by Th52;
      hence thesis by Th52;
    end;
    suppose
A1:   not B+^C c= A;
A2:   now
        assume A = B+^(A-^B);
        then not C c= A-^B by A1,ORDINAL2:33;
        hence A-^B-^C = {} by Def5;
      end;
      B c= A or not B c= A;
      then
A3:   A = B+^(A-^B) or A-^B = {} by Def5;
      A-^(B+^C) = {} by A1,Def5;
      hence thesis by A3,A2,Th56;
    end;
  end;
  hence thesis;
end;

theorem
  A c= B implies C-^B c= C-^A
proof
  assume
A1: A c= B;
  then
A2: B = A+^(B-^A) by Def5;
A3: now
    assume
A4: B c= C;
    then
A5: C = B+^(C-^B) by Def5;
    A c= C by A1,A4;
    then B+^(C-^B) = A+^(C-^A) by A5,Def5;
    then A+^((B-^A)+^(C-^B)) = A+^(C-^A) by A2,Th30;
    then (B-^A)+^(C-^B) = C-^A by Th21;
    hence thesis by Th24;
  end;
  not B c= C implies thesis by Def5;
  hence thesis by A3;
end;

theorem
  A c= B implies A-^C c= B-^C
proof
  assume
A1: A c= B;
A2: now
    assume
A3: C c= A;
    then
A4: A = C+^(A-^C) by Def5;
    C c= B by A1,A3;
    then C+^(A-^C) c= C+^(B-^C) by A1,A4,Def5;
    hence thesis by Th23;
  end;
  not C c= A implies thesis by Def5;
  hence thesis by A2;
end;

theorem
  C <> {} & A in B+^C implies A-^B in C
proof
  assume
A1: C <> {};
A2: B+^C-^B = C by Th52;
  not B c= A implies A-^B = {} by Def5;
  hence thesis by A1,A2,Th8,Th53;
end;

theorem
  A+^B in C implies B in C-^A
proof
A1: A+^B-^A = B by Th52;
  A c= A+^B by Th24;
  hence thesis by A1,Th53;
end;

theorem
  A c= B+^(A-^B)
proof
  now
    per cases;
    suppose
      B c= A;
      hence thesis by Def5;
    end;
    suppose
A1:   not B c= A;
      then A-^B = {} by Def5;
      hence thesis by A1,ORDINAL2:27;
    end;
  end;
  hence thesis;
end;

theorem
  A*^C -^ B*^C = (A-^B)*^C
proof
A1: now
    assume
A2: not B c= A;
    then
A3: not B*^C c= A*^C or C = {} by Th35;
A4: {}*^C = {} by ORDINAL2:35;
A5: A*^{} = {} by ORDINAL2:38;
    A-^B = {} by A2,Def5;
    hence thesis by A3,A5,A4,Def5,Th56;
  end;
  now
    assume B c= A;
    then A = B+^(A-^B) by Def5;
    then A*^C = B*^C+^(A-^B)*^C by Th46;
    hence thesis by Th52;
  end;
  hence thesis by A1;
end;

theorem Th64:
  (A div^ B)*^B c= A
proof
  now
    per cases;
    suppose
      B <> {};
      then ex C st A = (A div^ B)*^B+^C & C in B by Def6;
      hence thesis by Th24;
    end;
    suppose
      B = {};
      then A div^ B = {} by Def6;
      then (A div^ B)*^B = {} by ORDINAL2:35;
      hence thesis;
    end;
  end;
  hence thesis;
end;

theorem Th65:
  A = (A div^ B)*^B+^(A mod^ B)
proof
  (A div^ B)*^B c= A by Th64;
  hence thesis by Def5;
end;

theorem
  A = B*^C+^D & D in C implies B = A div^ C & D = A mod^ C
proof
  assume that
A1: A = B*^C+^D and
A2: D in C;
  thus B = A div^ C by A1,A2,Def6;
  hence thesis by A1,Th52;
end;

theorem
  A in B*^C implies A div^ C in B & A mod^ C in C
proof
A1: A = (A div^ C)*^C+^(A mod^ C) by Th65;
  assume
A2: A in B*^C;
  then C <> {} by ORDINAL2:38;
  then
A3: ex D st A = (A div^ C)*^C+^D & D in C by Def6;
  then
A4: (A div^ C)*^C c= A by Th24;
  assume not thesis;
  then B*^C c= (A div^ C)*^C by A3,A1,Th21,ORDINAL1:16,ORDINAL2:41;
  hence contradiction by A2,A4,ORDINAL1:5;
end;

theorem Th68:
  B <> {} implies A*^B div^ B = A
proof
  assume B <> {};
  then
A1: {} in B by Th8;
  A*^B = A*^B+^{} by ORDINAL2:27;
  hence thesis by A1,Def6;
end;

theorem
  A*^B mod^ B = {}
proof
A1: A*^{} = {} by ORDINAL2:38;
A2: A*^B-^A*^B = {} by Th54;
  {}-^(A*^B div^ B)*^B = {} by Th56;
  hence thesis by A1,A2,Th68;
end;

theorem
  {} div^ A = {} & {} mod^ A = {} & A mod^ {} = A
proof
A1: A = {} or A <> {};
  {} = {}*^A by ORDINAL2:35;
  hence {} div^ A = {} by A1,Def6,Th68;
  thus {} mod^ A = {} by Th56;
  thus A mod^ {} = A-^{} by ORDINAL2:38
    .= A by Th56;
end;

theorem
  A div^ 1 = A & A mod^ 1 = {}
proof
A1: A = A*^1 by ORDINAL2:39;
A2: A = A+^{} by ORDINAL2:27;
  1 = succ 0 .= { 0 };
  then
A3: {} in 1 by Th8;
  hence A div^ 1 = A by A1,A2,Def6;
  thus A mod^ 1 = A-^A by A1,A2,A3,Def6
    .= {} by Th54;
end;

begin :: Addenda
:: from ZF_REFLE, 2007.03.13, A.T.

theorem
  sup X c= succ union On X
proof
  reconsider A = union On X as Ordinal by Th5;
  On X c= succ A
  proof
    let x be object;
    assume
A1: x in On X;
    then reconsider a = x as Ordinal by ORDINAL1:def 9;
    a c= A by A1,ZFMISC_1:74;
    hence thesis by ORDINAL1:22;
  end;
  hence thesis by ORDINAL2:def 3;
end;

:: from ZFREFLE1, 2007.03.14, A.T.

reserve e,u for set;

theorem
  succ A is_cofinal_with 1
proof
  deffunc F(set) = A;
  consider psi such that
A1: dom psi = 1 & for B st B in 1 holds psi.B = F(B) from ORDINAL2:sch 3;
  take psi;
  thus dom psi = 1 by A1;
  thus rng psi c= succ A
  proof
    let e be object;
    assume e in rng psi;
    then consider u being object such that
A2: u in 1 and
A3: e = psi.u by A1,FUNCT_1:def 3;
    reconsider u as Ordinal by A2;
    psi.u = A by A1,A2;
    hence thesis by A3,ORDINAL1:6;
  end;
  thus psi is increasing
  by A1,Th14;
A4: psi.{} = A by A1,Lm1,ORDINAL1:6;
  rng psi = {psi.{}} by A1,Lm1,FUNCT_1:4;
  hence thesis by A4,ORDINAL2:23;
end;

:: from ARYTM_3, 2007.10.23, A.T.

theorem Th74:
  for a,b being Ordinal st a+^b is natural holds a in omega & b in omega
by Th24,ORDINAL1:12;

registration
  let a, b be natural Ordinal;
  cluster a -^ b -> natural;
  coherence
  proof
    not b c= a or b c= a;
    then a -^ b = {} or a = b+^(a-^b) by Def5;
    hence a-^b in omega by Th74,ORDINAL1:def 11;
  end;
  cluster a *^ b -> natural;
  coherence
  proof
    defpred P[natural Ordinal] means $1*^b is natural;
A1: now
      let a be natural Ordinal;
      assume P[a];
      then reconsider c = a*^b as natural Ordinal;
      (succ a)*^b = c+^b by ORDINAL2:36;
      hence P[succ a];
    end;
A2: P[0] by ORDINAL2:35;
    P[a] from ORDINAL2:sch 17(A2,A1);
    hence thesis;
  end;
end;

theorem
  for a,b being Ordinal st a*^b is natural non empty holds a in omega &
  b in omega
proof
  let x,y be Ordinal such that
A1: x*^y in omega;
  assume
A2: x*^y is non empty;
  then y <> {} by ORDINAL2:38;
  then
A3: x c= x*^y by Th36;
  x <> {} by A2,ORDINAL2:35;
  then y c= x*^y by Th36;
  hence thesis by A1,A3,ORDINAL1:12;
end;

definition
  let a,b be natural Ordinal;
  redefine func a+^b;  :: redefines +^ (ORDINAL2, definition)
  commutativity
  proof
    let a,b be natural Ordinal;
    defpred R[natural Ordinal] means a+^$1 = $1+^a;
A1: now
      let b be natural Ordinal;
      assume
A2:   R[b];
      defpred P[natural Ordinal] means (succ b)+^$1 = succ (b+^$1);
A3:   now
        let a be natural Ordinal;
        assume
A4:     P[a];
        (succ b)+^succ a = succ ((succ b)+^a) by ORDINAL2:28
          .= succ (b+^succ a) by A4,ORDINAL2:28;
        hence P[succ a];
      end;
      (succ b)+^{} = succ b by ORDINAL2:27
        .= succ (b+^{}) by ORDINAL2:27;
      then
A5:   P[0];
      P[a] from ORDINAL2:sch 17(A5,A3);
      hence R[succ b] by A2,ORDINAL2:28;
    end;
    a+^{} = a by ORDINAL2:27
      .= {}+^a by ORDINAL2:30;
    then
A6: R[0];
    thus R[b] from ORDINAL2:sch 17(A6,A1);
  end;
end;

definition
  let a,b be natural Ordinal;
  redefine func a*^b;  :: redefines *^ (ORDINAL2, definition)
  commutativity
  proof
    let a,b be natural Ordinal;
    defpred R[natural Ordinal] means a*^$1 = $1*^a;
A1: now
      let b be natural Ordinal;
      defpred P[natural Ordinal] means $1*^succ b = $1*^b+^$1;
      assume
A2:   R[b];
A3:   now
        let a be natural Ordinal;
        assume
A4:     P[a];
        (succ a)*^succ b = a*^(succ b)+^succ b by ORDINAL2:36
          .= a*^b+^(a+^succ b) by A4,Th30
          .= a*^b+^succ (a+^b) by ORDINAL2:28
          .= succ (a*^b+^(a+^b)) by ORDINAL2:28
          .= succ (a*^b+^b+^a) by Th30
          .= succ ((succ a)*^b+^a) by ORDINAL2:36
          .= (succ a)*^b+^succ a by ORDINAL2:28;
        hence P[succ a];
      end;
      {}*^succ b = {} by ORDINAL2:35
        .= {}+^{} by ORDINAL2:27
        .= {}*^b+^{} by ORDINAL2:35;
      then
A5:   P[0];
      P[a] from ORDINAL2:sch 17(A5,A3);
      hence R[succ b] by A2,ORDINAL2:36;
    end;
    a*^{} = {} by ORDINAL2:38
      .= {}*^a by ORDINAL2:35;
    then
A6: R[0];
    thus R[b] from ORDINAL2:sch 17(A6,A1);
  end;
end;