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

environ

 vocabularies ORDINAL2, ORDINAL1, FUNCT_1, XBOOLE_0, RELAT_1, TARSKI, ORDINAL3,
      SUBSET_1, CLASSES2, ZFMISC_1, CARD_1, ORDINAL4;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
      ORDINAL1, ORDINAL2, ORDINAL3, CARD_1, CLASSES2;
 constructors WELLORD2, FUNCOP_1, ORDINAL3, CARD_1, CLASSES1, CLASSES2,
      RELSET_1;
 registrations XBOOLE_0, FUNCT_1, ORDINAL1, ORDINAL2, ORDINAL3, CARD_1,
      CLASSES2, RELSET_1;
 requirements SUBSET, BOOLE, NUMERALS;
 definitions ORDINAL1, TARSKI, ORDINAL2, XBOOLE_0, RELAT_1;
 theorems ZFMISC_1, FUNCT_1, GRFUNC_1, ORDINAL1, ORDINAL2, ORDINAL3, CARD_2,
      CLASSES2, RELAT_1, CLASSES1, XBOOLE_0, XBOOLE_1, FUNCT_2, RELSET_1,
      CARD_1;
 schemes ORDINAL1, ORDINAL2, FINSET_1;

begin

reserve phi,fi,psi for Ordinal-Sequence,
  A,A1,B,C,D for Ordinal,
  f,g for Function,
  X for set,
  x,y,z for set;

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

Lm2: omega is limit_ordinal by ORDINAL1:def 11;

Lm3: 1 = succ {};

registration
  let L be Ordinal-Sequence;
  cluster last L -> ordinal;
  coherence;
end;

theorem
  dom fi = succ A implies last fi is_limes_of fi & lim fi = last fi
proof
  assume
A1: dom fi = succ A;
  then
A2: last fi = fi.A by ORDINAL2:6;
  thus last fi is_limes_of fi
  proof
    per cases;
    case
A3:   last fi = {};
      take A;
      thus A in dom fi by A1,ORDINAL1:6;
      let B;
      assume that
A4:   A c= B and
A5:   B in dom fi;
      B c= A by A1,A5,ORDINAL1:22;
      hence thesis by A2,A3,A4,XBOOLE_0:def 10;
    end;
    case
      last fi <> {};
      let B,C such that
A6:   B in last fi and
A7:   last fi in C;
      take A;
      thus A in dom fi by A1,ORDINAL1:6;
      let D;
      assume that
A8:   A c= D and
A9:   D in dom fi;
      D c= A by A1,A9,ORDINAL1:22;
      hence thesis by A2,A6,A7,A8,XBOOLE_0:def 10;
    end;
  end;
  hence thesis by ORDINAL2:def 10;
end;

definition
  let fi,psi be T-Sequence;
  func fi^psi -> T-Sequence means
  : Def1:
  dom it = (dom fi)+^(dom psi) & (for
A st A in dom fi holds it.A = fi.A) & for A st A in dom psi holds it.((dom fi)
  +^A) = psi.A;
  existence
  proof
    defpred P[set] means $1 in dom fi;
    deffunc G(Ordinal) = psi.(($1)-^dom fi);
    deffunc F(set) = fi.$1;
    consider f such that
A1: dom f = (dom fi)+^(dom psi) and
A2: for x being Ordinal st x in (dom fi)+^(dom psi) holds (P[x]
    implies f.x = F(x)) & (not P[x] implies f.x = G(x)) from FINSET_1:sch 1;
    reconsider f as T-Sequence by A1,ORDINAL1:def 7;
    take f;
    thus dom f = (dom fi)+^(dom psi) by A1;
    thus for A st A in dom fi holds f.A = fi.A
    proof
A3:   dom fi c= dom f by A1,ORDINAL3:24;
      let A;
      assume A in dom fi;
      hence thesis by A1,A2,A3;
    end;
    let A;
    dom fi c= (dom fi)+^A by ORDINAL3:24;
    then
A4: not (dom fi)+^A in dom fi by ORDINAL1:5;
    assume A in dom psi;
    then (dom fi)+^A in dom f by A1,ORDINAL2:32;
    then f.((dom fi)+^A) = psi.((((dom fi)+^A))-^dom fi) by A1,A2,A4;
    hence thesis by ORDINAL3:52;
  end;
  uniqueness
  proof
    let f1,f2 be T-Sequence such that
A5: dom f1 = (dom fi)+^(dom psi) and
A6: for A st A in dom fi holds f1.A = fi.A and
A7: for A st A in dom psi holds f1.((dom fi)+^A) = psi.A and
A8: dom f2 = (dom fi)+^(dom psi) and
A9: for A st A in dom fi holds f2.A = fi.A and
A10: for A st A in dom psi holds f2.((dom fi)+^A) = psi.A;
    now
      let x;
      assume
A11:  x in (dom fi)+^(dom psi);
      then reconsider A = x as Ordinal;
      now
        per cases;
        suppose
A12:      x in dom fi;
          then f1.A = fi.A by A6;
          hence f1.x = f2.x by A9,A12;
        end;
        suppose
          not x in dom fi;
          then dom fi c= A by ORDINAL1:16;
          then
A13:      (dom fi)+^(A-^dom fi) = A by ORDINAL3:def 5;
          then f1.A = psi.(A-^dom fi) by A7,A11,ORDINAL3:22;
          hence f1.x = f2.x by A10,A11,A13,ORDINAL3:22;
        end;
      end;
      hence f1.x = f2.x;
    end;
    hence thesis by A5,A8,FUNCT_1:2;
  end;
end;

theorem Th2:
 rng(fi^psi) c= rng fi \/ rng psi
   proof set f = fi^psi, A1 = rng fi, A2 = rng psi;
A1:  dom(fi^psi) = (dom fi)+^(dom psi) by Def1;
    let y;
      assume y in rng f;
      then consider x such that
A2:   x in dom f and
A3:   y = f.x by FUNCT_1:def 3;
      reconsider x as Ordinal by A2;
        per cases;
        suppose
A4:       x in dom fi;
          then
A5:       fi.x in rng fi by FUNCT_1:def 3;
          y = fi.x by A3,A4,Def1;
          then y in A1 by A5;
          hence thesis by XBOOLE_0:def 3;
        end;
        suppose
          not x in dom fi;
          then dom fi c= x by ORDINAL1:16;
          then
A6:      (dom fi)+^(x-^dom fi) = x by ORDINAL3:def 5;
          then
A7:      x-^dom fi in dom psi by A1,A2,ORDINAL3:22;
          then y = psi.(x-^dom fi) by A3,A6,Def1;
          then y in rng psi by A7,FUNCT_1:def 3;
          then y in A2;
          hence thesis by XBOOLE_0:def 3;
        end;
    end;

registration
  let fi,psi;
  cluster fi^psi -> Ordinal-yielding;
  coherence
  proof
    set f = fi^psi;
    consider A1 being Ordinal such that
A1: rng fi c= A1 by ORDINAL2:def 4;
    consider A2 being Ordinal such that
A2: rng psi c= A2 by ORDINAL2:def 4;
A3:   A2 c= A1+^A2 by ORDINAL3:24;
   A1 c= A1+^A2 by ORDINAL3:24;
    then
A4:   A1 \/ A2 c= A1+^A2 by A3,XBOOLE_1:8;
A5:  rng f c= rng fi \/ rng psi by Th2;
    rng fi \/ rng psi c= A1 \/ A2 by A1,A2,XBOOLE_1:13;
    then rng f c= A1 \/ A2 by A5,XBOOLE_1:1;
    then rng f c= A1+^A2 by A4,XBOOLE_1:1;
    hence thesis by ORDINAL2:def 4;
  end;
end;

theorem Th3:
  A is_limes_of psi implies A is_limes_of fi^psi
proof
  assume that
A1: A = {} & (ex B st B in dom psi & for C st B c= C & C in dom psi
holds psi.C = {}) or A <> {} & for B,C st B in A & A in C ex D st D in dom psi
  & for E being Ordinal st D c= E & E in dom psi holds B in psi.E & psi.E in C;
A2: dom(fi^psi) = (dom fi)+^(dom psi) by Def1;
  per cases;
  case
    A = {};
    then consider B such that
A3: B in dom psi and
A4: for C st B c= C & C in dom psi holds psi.C = {} by A1;
    take B1 = (dom fi)+^B;
    thus B1 in dom(fi^psi) by A2,A3,ORDINAL2:32;
    let C;
    assume that
A5: B1 c= C and
A6: C in dom(fi^psi);
A7: C = B1+^(C-^B1) by A5,ORDINAL3:def 5
      .= (dom fi)+^(B+^(C-^B1)) by ORDINAL3:30;
    then
A8: B+^(C-^B1) in dom psi by A2,A6,ORDINAL3:22;
    B c= B+^(C-^B1) by ORDINAL3:24;
    then psi.(B+^(C-^B1)) = {} by A2,A4,A6,A7,ORDINAL3:22;
    hence thesis by A7,A8,Def1;
  end;
  case
    A <> {};
    let B,C;
    assume that
A9: B in A and
A10: A in C;
    consider D such that
A11: D in dom psi and
A12: for E being Ordinal st D c= E & E in dom psi holds B in psi.E &
    psi.E in C by A1,A9,A10;
    take D1 = (dom fi)+^D;
    thus D1 in dom(fi^psi) by A2,A11,ORDINAL2:32;
    let E be Ordinal;
    assume that
A13: D1 c= E and
A14: E in dom(fi^psi);
A15: D c= D+^(E-^D1) by ORDINAL3:24;
A16: E = D1+^(E-^D1) by A13,ORDINAL3:def 5
      .= (dom fi)+^(D+^(E-^D1)) by ORDINAL3:30;
    then
A17: D+^(E-^D1) in dom psi by A2,A14,ORDINAL3:22;
    then (fi^psi).E = psi.(D+^(E-^D1)) by A16,Def1;
    hence thesis by A12,A15,A17;
  end;
end;

theorem
  A is_limes_of fi implies B+^A is_limes_of B+^fi
proof
  assume that
A1: A = {} & (ex B st B in dom fi & for C st B c= C & C in dom fi holds
fi.C = {}) or A <> {} & 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;
A2: dom fi = dom(B+^fi) by ORDINAL3:def 1;
  per cases;
  case
A3: B+^A = {};
    then consider A1 such that
A4: A1 in dom fi and
A5: for C st A1 c= C & C in dom fi holds fi.C = {} by A1,ORDINAL3:26;
    take A1;
    thus A1 in dom(B+^fi) by A4,ORDINAL3:def 1;
    let C;
    assume that
A6: A1 c= C and
A7: C in dom(B+^fi);
A8: (B+^fi).C = B+^(fi.C) by A2,A7,ORDINAL3:def 1;
    fi.C = {} by A2,A5,A6,A7;
    hence thesis by A3,A8,ORDINAL3:26;
  end;
  case
    B+^A <> {};
    now
      per cases;
      suppose
A9:     A = {};
        then consider A1 such that
A10:    A1 in dom fi and
A11:    for C st A1 c= C & C in dom fi holds fi.C = {} by A1;
        let B1,B2 be Ordinal such that
A12:    B1 in B+^A and
A13:    B+^A in B2;
        take A1;
        thus A1 in dom(B+^fi) by A10,ORDINAL3:def 1;
        let C;
        assume that
A14:    A1 c= C and
A15:    C in dom(B+^fi);
        (B+^fi).C = B+^(fi.C) by A2,A15,ORDINAL3:def 1;
        hence B1 in (B+^fi).C & (B+^fi).C in B2 by A2,A9,A11,A12,A13,A14,A15;
      end;
      suppose
A16:    A <> {};
        let B1,B2 be Ordinal;
        assume that
A17:    B1 in B+^A and
A18:    B+^A in B2;
        B1-^B in A by A16,A17,ORDINAL3:60;
        then consider A1 such that
A19:    A1 in dom fi and
A20:    for C st A1 c= C & C in dom fi holds B1-^B in fi.C & fi.C in
        B2-^B by A1,A18,ORDINAL3:61;
A21:    B1 c= B+^(B1-^B) by ORDINAL3:62;
A22:    B c= B+^A by ORDINAL3:24;
        B+^A c= B2 by A18,ORDINAL1:def 2;
        then B c= B2 by A22,XBOOLE_1:1;
        then
A23:    B+^(B2-^B) = B2 by ORDINAL3:def 5;
        take A1;
        thus A1 in dom(B+^fi) by A19,ORDINAL3:def 1;
        let C;
        assume that
A24:    A1 c= C and
A25:    C in dom(B+^fi);
A26:    (B+^fi).C = B+^(fi.C) by A2,A25,ORDINAL3:def 1;
        reconsider E = fi.C as Ordinal;
        B1-^B in E by A2,A20,A24,A25;
        then
A27:    B+^(B1-^B) in B+^E by ORDINAL2:32;
        E in B2-^B by A2,A20,A24,A25;
        hence B1 in (B+^fi).C & (B+^fi).C in B2 by A21,A26,A23,A27,ORDINAL1:12
,ORDINAL2:32;
      end;
    end;
    hence thesis;
  end;
end;

Lm4: A is_limes_of fi implies dom fi <> {}
proof
  assume that
A1: A = {} & (ex B st B in dom fi & for C st B c= C & C in dom fi holds
fi.C = {}) or A <> {} & 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;
  now
    per cases;
    suppose
      A = {};
      hence thesis by A1;
    end;
    suppose
      A <> {};
      then {} in A by ORDINAL3:8;
      then
      ex B st B in dom fi & for C st B c= C & C in dom fi holds {} in fi.C
      & fi.C in succ A by A1,ORDINAL1:6;
      hence thesis;
    end;
  end;
  hence thesis;
end;

theorem Th5:
  A is_limes_of fi implies A*^B is_limes_of fi*^B
proof
A1: dom fi = dom(fi*^B) by ORDINAL3:def 4;
  assume
A2: A is_limes_of fi;
  then
A3: dom fi <> {} by Lm4;
  per cases;
  case
    A*^B = {};
    then
A4: B = {} or A = {} by ORDINAL3:31;
    now
      per cases;
      suppose
A5:     B = {};
        set x = the Element of dom fi;
        reconsider x as Ordinal;
        take A1 = x;
        thus A1 in dom(fi*^B) by A1,A3;
        let C;
        assume that
        A1 c= C and
A6:     C in dom(fi*^B);
        thus (fi*^B).C = (fi.C)*^B by A1,A6,ORDINAL3:def 4
          .= {} by A5,ORDINAL2:38;
      end;
      suppose
        B <> {};
        then consider A1 such that
A7:     A1 in dom fi and
A8:     for C st A1 c= C & C in dom fi holds fi.C = {} by A2,A4,ORDINAL2:def 9
;
        take A1;
        thus A1 in dom(fi*^B) by A7,ORDINAL3:def 4;
        let C;
        assume that
A9:     A1 c= C and
A10:    C in dom(fi*^B);
A11:    (fi*^B).C = (fi.C)*^B by A1,A10,ORDINAL3:def 4;
        fi.C = {} by A1,A8,A9,A10;
        hence (fi*^B).C = {} by A11,ORDINAL2:35;
      end;
    end;
    hence thesis;
  end;
  case
A12: A*^B <> {};
    let B1,B2 be Ordinal such that
A13: B1 in A*^B and
A14: A*^B in B2;
A15: B <> {} by A12,ORDINAL2:38;
A16: now
      assume not ex A1 st A = succ A1;
      then A is limit_ordinal by ORDINAL1:29;
      then consider C such that
A17:  C in A and
A18:  B1 in C*^B by A13,ORDINAL3:41;
      A in succ A by ORDINAL1:6;
      then consider D such that
A19:  D in dom fi and
A20:  for A1 st D c= A1 & A1 in dom fi holds C in fi.A1 & fi.A1 in
      succ A by A2,A17,ORDINAL2:def 9;
      take D;
      thus D in dom(fi*^B) by A19,ORDINAL3:def 4;
      let A1;
      assume that
A21:  D c= A1 and
A22:  A1 in dom(fi*^B);
      reconsider E = fi.A1 as Ordinal;
      fi.A1 in succ A by A1,A20,A21,A22;
      then
A23:  E c= A by ORDINAL1:22;
      C in fi.A1 by A1,A20,A21,A22;
      then C*^B in E*^B by A15,ORDINAL2:40;
      then
A24:  B1 in E*^B by A18,ORDINAL1:10;
      (fi*^B).A1 = (fi.A1)*^B by A1,A22,ORDINAL3:def 4;
      hence B1 in (fi*^B).A1 & (fi*^B).A1 in B2 by A14,A23,A24,ORDINAL1:12
,ORDINAL2:41;
    end;
    now
A25:  A in succ A by ORDINAL1:6;
      given A1 such that
A26:  A = succ A1;
      A1 in A by A26,ORDINAL1:6;
      then consider D such that
A27:  D in dom fi and
A28:  for C st D c= C & C in dom fi holds A1 in fi.C & fi.C in succ A
      by A2,A25,ORDINAL2:def 9;
      take D;
      thus D in dom(fi*^B) by A27,ORDINAL3:def 4;
      let C;
      assume that
A29:  D c= C and
A30:  C in dom(fi*^B);
      reconsider E = fi.C as Ordinal;
      A1 in E by A1,A28,A29,A30;
      then
A31:  A c= E by A26,ORDINAL1:21;
      E in succ A by A1,A28,A29,A30;
      then
A32:  E c= A by ORDINAL1:22;
      (fi*^B).C = E*^B by A1,A30,ORDINAL3:def 4;
      hence B1 in (fi*^B).C & (fi*^B).C in B2 by A13,A14,A31,A32,
XBOOLE_0:def 10;
    end;
    hence thesis by A16;
  end;
end;

theorem Th6:
  dom fi = dom psi & B is_limes_of fi & C is_limes_of psi & ((for A
st A in dom fi holds fi.A c= psi.A) or for A st A in dom fi holds fi.A in psi.A
  ) implies B c= C
proof
  assume that
A1: dom fi = dom psi and
A2: B = {} & (ex A1 st A1 in dom fi & for C st A1 c= C & C in dom fi
holds fi.C = {}) or B <> {} & for A1,C st A1 in B & B in C ex D st D in dom fi
  & for E being Ordinal st D c= E & E in dom fi holds A1 in fi.E & fi.E in C
  and
A3: C = {} & (ex B st B in dom psi & for A1 st B c= A1 & A1 in dom psi
  holds psi.A1 = {}) or C <> {} & for B,A1 st B in C & C in A1 ex D st D in dom
psi & for E being Ordinal st D c= E & E in dom psi holds B in psi.E & psi.E in
  A1 and
A4: (for A st A in dom fi holds fi.A c= psi.A) or for A st A in dom fi
  holds fi.A in psi.A;
A5: now
    let A;
    reconsider A1 = fi.A, A2 = psi.A as Ordinal;
    assume A in dom fi;
    then A1 c= A2 or A1 in A2 by A4;
    hence fi.A c= psi.A by ORDINAL1:def 2;
  end;
  now
    per cases;
    suppose
      B = {} & C = {};
      hence thesis;
    end;
    suppose
      B = {} & C <> {};
      then B in C by ORDINAL3:8;
      hence thesis by ORDINAL1:def 2;
    end;
    suppose
A6:   B <> {} & C = {};
      then {} in B by ORDINAL3:8;
      then consider A2 being Ordinal such that
A7:   A2 in dom fi and
A8:   for A st A2 c= A & A in dom fi holds {} in fi.A & fi.A in succ
      B by A2,ORDINAL1:6;
      consider A1 such that
A9:   A1 in dom psi and
A10:  for A st A1 c= A & A in dom psi holds psi.A = {} by A3,A6;
A11:  A1 \/ A2 = A1 or A1 \/ A2 = A2 by ORDINAL3:12;
      then
A12:  fi.(A1 \/ A2) c= psi.(A1 \/ A2) by A1,A5,A9,A7;
      A2 c= A1 \/ A2 by XBOOLE_1:7;
      then {} in fi.(A1 \/ A2) by A1,A9,A7,A8,A11;
      hence thesis by A1,A9,A10,A7,A11,A12,XBOOLE_1:7;
    end;
    suppose
A13:  B <> {} & C <> {};
      assume not B c= C;
      then C in B by ORDINAL1:16;
      then consider A1 such that
A14:  A1 in dom fi and
A15:  for A st A1 c= A & A in dom fi holds C in fi.A & fi.A in succ B
      by A2,ORDINAL1:6;
      {} in C by A13,ORDINAL3:8;
      then consider A2 being Ordinal such that
A16:  A2 in dom psi and
A17:  for A st A2 c= A & A in dom psi holds {} in psi.A & psi.A in
      succ C by A3,ORDINAL1:6;
A18:  A1 \/ A2 = A1 or A1 \/ A2 = A2 by ORDINAL3:12;
      reconsider A3 = psi.(A1 \/ A2) as Ordinal;
      A2 c= A1 \/ A2 by XBOOLE_1:7;
      then psi.(A1 \/ A2) in succ C by A1,A14,A16,A17,A18;
      then
A19:  A3 c= C by ORDINAL1:22;
      A1 c= A1 \/ A2 by XBOOLE_1:7;
      then
A20:  C in fi.(A1 \/ A2) by A1,A14,A15,A16,A18;
      fi.(A1 \/ A2) c= psi.(A1 \/ A2) by A1,A5,A14,A16,A18;
      hence contradiction by A20,A19,ORDINAL1:5;
    end;
  end;
  hence thesis;
end;

reserve f1,f2 for Ordinal-Sequence;

theorem
  dom f1 = dom fi & dom fi = dom f2 & A is_limes_of f1 & A is_limes_of
  f2 & (for A st A in dom fi holds f1.A c= fi.A & fi.A c= f2.A) implies A
  is_limes_of fi
proof
  assume that
A1: dom f1 = dom fi and
A2: dom fi = dom f2 and
A3: A = {} & (ex B st B in dom f1 & for C st B c= C & C in dom f1 holds
f1.C = {}) or A <> {} & for B,C st B in A & A in C ex D st D in dom f1 & for E
  being Ordinal st D c= E & E in dom f1 holds B in f1.E & f1.E in C and
A4: A = {} & (ex B st B in dom f2 & for C st B c= C & C in dom f2 holds
f2.C = {}) or A <> {} & for B,C st B in A & A in C ex D st D in dom f2 & for E
  being Ordinal st D c= E & E in dom f2 holds B in f2.E & f2.E in C and
A5: for A st A in dom fi holds f1.A c= fi.A & fi.A c= f2.A;
  per cases;
  case
    A = {};
    then consider B being Ordinal such that
A6: B in dom f2 and
A7: for C st B c= C & C in dom f2 holds f2.C = {} by A4;
    take B;
    thus B in dom fi by A2,A6;
    let C;
    assume that
A8: B c= C and
A9: C in dom fi;
    f2.C = {} by A2,A7,A8,A9;
    hence thesis by A5,A9,XBOOLE_1:3;
  end;
  case
    A <> {};
    let B,C;
    assume that
A10: B in A and
A11: A in C;
    consider D2 being Ordinal such that
A12: D2 in dom f2 and
A13: for A1 st D2 c= A1 & A1 in dom f2 holds B in f2.A1 & f2.A1 in C
    by A4,A10,A11;
    consider D1 being Ordinal such that
A14: D1 in dom f1 and
A15: for A1 st D1 c= A1 & A1 in dom f1 holds B in f1.A1 & f1.A1 in C
    by A3,A10,A11;
    take D = D1 \/ D2;
    thus D in dom fi by A1,A2,A14,A12,ORDINAL3:12;
    let A1;
    assume that
A16: D c= A1 and
A17: A1 in dom fi;
    reconsider B1 = fi.A1, B2 = f2.A1 as Ordinal;
A18: B1 c= B2 by A5,A17;
    D2 c= D by XBOOLE_1:7;
    then D2 c= A1 by A16,XBOOLE_1:1;
    then
A19: B2 in C by A2,A13,A17;
    D1 c= D by XBOOLE_1:7;
    then D1 c= A1 by A16,XBOOLE_1:1;
    then
A20: B in f1.A1 by A1,A15,A17;
    f1.A1 c= fi.A1 by A5,A17;
    hence thesis by A20,A18,A19,ORDINAL1:12;
  end;
end;

theorem Th8:
  dom fi <> {} & dom fi is limit_ordinal & fi is increasing implies
  sup fi is_limes_of fi & lim fi = sup fi
proof
  assume that
A1: dom fi <> {} & dom fi is limit_ordinal and
A2: A in B & B in dom fi implies fi.A in fi.B;
  reconsider x = fi.{} as Ordinal;
  {} in dom fi by A1,ORDINAL3:8;
  then
A3: x in rng fi by FUNCT_1:def 3;
  thus sup fi is_limes_of fi
  proof
    per cases;
    case
      sup fi = {};
      hence thesis by A3,ORDINAL2:19;
    end;
    case
      sup fi <> {};
      let A,B;
      assume that
A4:   A in sup fi and
A5:   sup fi in B;
      consider C such that
A6:   C in rng fi and
A7:   A c= C by A4,ORDINAL2:21;
      consider x such that
A8:   x in dom fi and
A9:   C = fi.x by A6,FUNCT_1:def 3;
      reconsider x as Ordinal by A8;
      take M = succ x;
      thus M in dom fi by A1,A8,ORDINAL1:28;
      let D;
      assume that
A10:  M c= D and
A11:  D in dom fi;
      reconsider E = fi.D as Ordinal;
      x in M by ORDINAL1:6;
      then C in E by A2,A9,A10,A11;
      hence A in fi.D by A7,ORDINAL1:12;
      fi.D in rng fi by A11,FUNCT_1:def 3;
      then E in sup fi by ORDINAL2:19;
      hence thesis by A5,ORDINAL1:10;
    end;
  end;
  hence thesis by ORDINAL2:def 10;
end;

theorem Th9:
  fi is increasing & A c= B & B in dom fi implies fi.A c= fi.B
proof
  assume that
A1: for A,B st A in B & B in dom fi holds fi.A in fi.B and
A2: A c= B and
A3: B in dom fi;
  reconsider C = fi.B as Ordinal;
  now
    per cases;
    suppose
      A = B;
      hence thesis;
    end;
    suppose
      A <> B;
      then A c< B by A2,XBOOLE_0:def 8;
      then A in B by ORDINAL1:11;
      then fi.A in C by A1,A3;
      hence thesis by ORDINAL1:def 2;
    end;
  end;
  hence thesis;
end;

theorem Th10:
  fi is increasing & A in dom fi implies A c= fi.A
proof
  assume that
A1: for A,B st A in B & B in dom fi holds fi.A in fi.B and
A2: A in dom fi and
A3: not A c= fi.A;
  defpred P[set] means $1 in dom fi & not $1 c= fi.$1;
A4: ex A st P[A] by A2,A3;
  consider A such that
A5: P[A] and
A6: for B st P[B] holds A c= B from ORDINAL1:sch 1(A4);
  reconsider B = fi.A as Ordinal;
A7: B in A by A5,ORDINAL1:16;
  then not B c= fi.B by A1,A5,ORDINAL1:5;
  hence contradiction by A5,A6,A7,ORDINAL1:10;
end;

theorem Th11:
  phi is increasing implies phi"A is Ordinal
proof
  assume
A1: for A,B st A in B & B in dom phi holds phi.A in phi.B;
  now
    let X;
    assume
A2: X in phi"A;
    then
A3: X in dom phi by FUNCT_1:def 7;
    hence X is Ordinal;
    reconsider B = X as Ordinal by A3;
A4: phi.X in A by A2,FUNCT_1:def 7;
    thus X c= phi"A
    proof
      let x;
      assume
A5:   x in X;
      then x in B;
      then reconsider C = x, D = phi.B as Ordinal;
      reconsider E = phi.C as Ordinal;
      E in D by A1,A3,A5;
      then
A6:   phi.x in A by A4,ORDINAL1:10;
      C in dom phi by A3,A5,ORDINAL1:10;
      hence thesis by A6,FUNCT_1:def 7;
    end;
  end;
  hence thesis by ORDINAL1:19;
end;

theorem Th12:
  f1 is increasing implies f2*f1 is Ordinal-Sequence
proof
A1: dom(f2*f1) = f1"dom f2 by RELAT_1:147;
  assume f1 is increasing;
  then dom(f2*f1) is Ordinal by A1,Th11;
  then reconsider f = f2*f1 as T-Sequence by ORDINAL1:def 7;
  consider A such that
A2: rng f2 c= A by ORDINAL2:def 4;
  rng f c= rng f2 by RELAT_1:26;
  then rng f c= A by A2,XBOOLE_1:1;
  hence thesis by ORDINAL2:def 4;
end;

theorem Th13:
  f1 is increasing & f2 is increasing implies ex phi st phi = f1*
  f2 & phi is increasing
proof
  assume that
A1: f1 is increasing and
A2: f2 is increasing;
  reconsider f = f1*f2 as Ordinal-Sequence by A2,Th12;
  take f;
  thus f = f1*f2;
  let A,B;
  assume that
A3: A in B and
A4: B in dom f;
  reconsider A1 = f2.A, B1 = f2.B as Ordinal;
A5: B1 in dom f1 by A4,FUNCT_1:11;
  dom f c= dom f2 by RELAT_1:25;
  then
A6: A1 in B1 by A2,A3,A4,ORDINAL2:def 12;
A7: f.B = f1.B1 by A4,FUNCT_1:12;
  f.A = f1.A1 by A3,A4,FUNCT_1:12,ORDINAL1:10;
  hence thesis by A1,A6,A5,A7,ORDINAL2:def 12;
end;

theorem Th14:
  f1 is increasing & A is_limes_of f2 & sup rng f1 = dom f2 & fi =
  f2*f1 implies A is_limes_of fi
proof
  assume that
A1: f1 is increasing and
A2: A = {} & (ex B st B in dom f2 & for C st B c= C & C in dom f2 holds
f2.C = {}) or A <> {} & for B,C st B in A & A in C ex D st D in dom f2 & for E
  being Ordinal st D c= E & E in dom f2 holds B in f2.E & f2.E in C and
A3: sup rng f1 = dom f2 and
A4: fi = f2*f1;
  per cases;
  case
    A = {};
    then consider B such that
A5: B in dom f2 and
A6: for C st B c= C & C in dom f2 holds f2.C = {} by A2;
    consider B1 being Ordinal such that
A7: B1 in rng f1 and
A8: B c= B1 by A3,A5,ORDINAL2:21;
    consider x such that
A9: x in dom f1 and
A10: B1 = f1.x by A7,FUNCT_1:def 3;
    reconsider x as Ordinal by A9;
    take x;
    B1 in dom f2 by A3,A7,ORDINAL2:19;
    hence x in dom fi by A4,A9,A10,FUNCT_1:11;
    let C such that
A11: x c= C and
A12: C in dom fi;
    reconsider C1 = f1.C as Ordinal;
A13: dom fi c= dom f1 by A4,RELAT_1:25;
    then B1 c= C1 by A1,A10,A11,A12,Th9;
    then
A14: B c= C1 by A8,XBOOLE_1:1;
    C1 in rng f1 by A12,A13,FUNCT_1:def 3;
    then f2.C1 = {} by A3,A6,A14,ORDINAL2:19;
    hence thesis by A4,A12,FUNCT_1:12;
  end;
  case
    A <> {};
    let B,C;
    assume that
A15: B in A and
A16: A in C;
    consider D such that
A17: D in dom f2 and
A18: for A1 st D c= A1 & A1 in dom f2 holds B in f2.A1 & f2.A1 in C by A2,A15
,A16;
    consider B1 being Ordinal such that
A19: B1 in rng f1 and
A20: D c= B1 by A3,A17,ORDINAL2:21;
    consider x such that
A21: x in dom f1 and
A22: B1 = f1.x by A19,FUNCT_1:def 3;
    reconsider x as Ordinal by A21;
    take x;
    B1 in dom f2 by A3,A19,ORDINAL2:19;
    hence x in dom fi by A4,A21,A22,FUNCT_1:11;
    let E be Ordinal such that
A23: x c= E and
A24: E in dom fi;
    reconsider E1 = f1.E as Ordinal;
A25: dom fi c= dom f1 by A4,RELAT_1:25;
    then E1 in rng f1 by A24,FUNCT_1:def 3;
    then
A26: E1 in dom f2 by A3,ORDINAL2:19;
    B1 c= E1 by A1,A22,A23,A24,A25,Th9;
    then
A27: D c= E1 by A20,XBOOLE_1:1;
    then
A28: f2.E1 in C by A18,A26;
    B in f2.E1 by A18,A27,A26;
    hence thesis by A4,A24,A28,FUNCT_1:12;
  end;
end;

theorem Th15:
  phi is increasing implies phi|A is increasing
proof
  assume
A1: for A,B st A in B & B in dom phi holds phi.A in phi.B;
  let B,C such that
A2: B in C and
A3: C in dom (phi|A);
A4: phi.B = (phi|A).B by A2,A3,FUNCT_1:47,ORDINAL1:10;
  dom (phi|A) c= dom phi by RELAT_1:60;
  then phi.B in phi.C by A1,A2,A3;
  hence thesis by A3,A4,FUNCT_1:47;
end;

theorem Th16:
  phi is increasing & dom phi is limit_ordinal implies sup phi is limit_ordinal
proof
  assume that
A1: phi is increasing and
A2: dom phi is limit_ordinal;
  now
    let A;
    assume A in sup phi;
    then consider B such that
A3: B in rng phi and
A4: A c= B by ORDINAL2:21;
    consider x such that
A5: x in dom phi and
A6: B = phi.x by A3,FUNCT_1:def 3;
    reconsider x as Ordinal by A5;
A7: succ x in dom phi by A2,A5,ORDINAL1:28;
    reconsider C = phi.succ x as Ordinal;
    x in succ x by ORDINAL1:6;
    then B in C by A1,A6,A7,ORDINAL2:def 12;
    then
A8: succ B c= C by ORDINAL1:21;
A9: succ A c= succ B by A4,ORDINAL2:1;
    C in rng phi by A7,FUNCT_1:def 3;
    then C in sup phi by ORDINAL2:19;
    then succ B in sup phi by A8,ORDINAL1:12;
    hence succ A in sup phi by A9,ORDINAL1:12;
  end;
  hence thesis by ORDINAL1:28;
end;

Lm5: rng f c= X implies (g|X)*f = g*f
proof
A1: f"rng f = dom f by RELAT_1:134;
  assume rng f c= X;
  then
A2: f"rng f c= f"X by RELAT_1:143;
  f"X c= dom f by RELAT_1:132;
  then
A3: f"X = dom f by A2,A1,XBOOLE_0:def 10;
  dom ((g|X)*f) = f"(dom (g|X)) by RELAT_1:147
    .= f"(dom g /\ X) by RELAT_1:61
    .= f"(dom g) /\ f"X by FUNCT_1:68
    .= f"(dom g) by A3,RELAT_1:132,XBOOLE_1:28
    .= dom (g*f) by RELAT_1:147;
  hence thesis by GRFUNC_1:3,RELAT_1:64;
end;

theorem
  fi is increasing & fi is continuous & psi is continuous & phi = psi*fi
  implies phi is continuous
proof
  assume that
A1: fi is increasing and
A2: for A,B st A in dom fi & A <> {} & A is limit_ordinal & B = fi.A
  holds B is_limes_of fi|A and
A3: for A,B st A in dom psi & A <> {} & A is limit_ordinal & B = psi.A
  holds B is_limes_of psi|A and
A4: phi = psi*fi;
  let A,B such that
A5: A in dom phi and
A6: A <> {} and
A7: A is limit_ordinal and
A8: B = phi.A;
  reconsider A1 = fi.A as Ordinal;
A9: fi|A is increasing by A1,Th15;
A10: dom phi c= dom fi by A4,RELAT_1:25;
  then A c= dom fi by A5,ORDINAL1:def 2;
  then
A11: dom (fi|A) = A by RELAT_1:62;
  A1 is_limes_of fi|A by A2,A5,A6,A7,A10;
  then lim (fi|A) = A1 by ORDINAL2:def 10;
  then
A12: sup (fi|A) = A1 by A6,A7,A11,A9,Th8;
A13: B = psi.A1 by A4,A5,A8,FUNCT_1:12;
A14: {} in A by A6,ORDINAL3:8;
A15: A1 in dom psi by A4,A5,FUNCT_1:11;
  then A1 c= dom psi by ORDINAL1:def 2;
  then
A16: dom (psi|A1) = A1 by RELAT_1:62;
A17: rng (fi|A) c= sup rng (fi|A)
  proof
    let x;
    assume
A18: x in rng (fi|A);
    then ex y st y in dom (fi|A) & x = (fi|A).y by FUNCT_1:def 3;
    hence thesis by A18,ORDINAL2:19;
  end;
  phi|A = psi*(fi| A ) by A4,RELAT_1:83;
  then
A19: phi|A = (psi|A1)*(fi|A) by A17,A12,Lm5;
  A c= A1 by A1,A5,A10,Th10;
  then B is_limes_of psi|A1 by A3,A7,A13,A15,A11,A14,A9,A12,Th16;
  hence thesis by A9,A16,A12,A19,Th14;
end;

theorem
  (for A st A in dom fi holds fi.A = C+^A) implies fi is increasing
proof
  assume
A1: for A st A in dom fi holds fi.A = C+^A;
  let A,B;
  assume that
A2: A in B and
A3: B in dom fi;
A4: fi.B = C+^B by A1,A3;
  fi.A = C+^A by A1,A2,A3,ORDINAL1:10;
  hence thesis by A2,A4,ORDINAL2:32;
end;

theorem Th19:
  C <> {} & (for A st A in dom fi holds fi.A = A*^C) implies fi is increasing
proof
  assume that
A1: C <> {} and
A2: for A st A in dom fi holds fi.A = A*^C;
  let A,B;
  assume that
A3: A in B and
A4: B in dom fi;
A5: fi.B = B*^C by A2,A4;
  fi.A = A*^C by A2,A3,A4,ORDINAL1:10;
  hence thesis by A1,A3,A5,ORDINAL2:40;
end;

theorem Th20:
  A <> {} implies exp({},A) = {}
proof
  defpred FF[Ordinal] means $1 <> {} implies exp({},$1) = {};
A1: FF[B] implies FF[succ B]
  proof
    assume that
    FF[B] and
    succ B <> {};
    thus exp({},succ B) = {}*^exp({},B) by ORDINAL2:44
      .= {} by ORDINAL2:35;
  end;
A2: for B st B <> {} & B is limit_ordinal & for C st C in B holds FF[C]
  holds FF[B]
  proof
    deffunc F(Ordinal) = exp({},$1);
    let A such that
A3: A <> {} and
A4: A is limit_ordinal and
A5: for C st C in A holds FF[C] and
    A <> {};
    consider fi such that
A6: dom fi = A & for B st B in A holds fi.B = F(B) from ORDINAL2:sch 3;
    {} is_limes_of fi
    proof
      per cases;
      case
        {} = {};
        take B = 1;
        {} in A by A3,ORDINAL3:8;
        hence B in dom fi by A4,A6,Lm3,ORDINAL1:28;
        let D;
        assume
A7:     B c= D;
        assume
A8:     D in dom fi;
        then FF[D] by A5,A6;
        hence thesis by A6,A7,A8,Lm3,ORDINAL1:21;
      end;
      case
        {} <> {};
        thus thesis;
      end;
    end;
    then lim fi = {} by ORDINAL2:def 10;
    hence thesis by A3,A4,A6,ORDINAL2:45;
  end;
A9: FF[{}];
  FF[B] from ORDINAL2:sch 1(A9,A1,A2);
  hence thesis;
end;

Lm6: A <> {} & A is limit_ordinal implies for fi st dom fi = A & for B st B in
A holds fi.B = exp({},B) holds {} is_limes_of fi
proof
  assume that
A1: A <> {} and
A2: A is limit_ordinal;
  let fi;
  assume that
A3: dom fi = A and
A4: for B st B in A holds fi.B = exp({},B);
  per cases;
  case
    {} = {};
    take B = 1;
    {} in A by A1,ORDINAL3:8;
    hence B in dom fi by A2,A3,Lm3,ORDINAL1:28;
    let D;
    assume that
A5: B c= D and
A6: D in dom fi;
A7: D <> {} by A5,Lm3,ORDINAL1:21;
    exp({},D) = fi.D by A3,A4,A6;
    hence thesis by A7,Th20;
  end;
  case
    {} <> {};
    thus thesis;
  end;
end;

Lm7: A <> {} implies for fi st dom fi = A & for B st B in A holds fi.B = exp(1
,B) holds 1 is_limes_of fi
proof
  assume that
A1: A <> {};
  let fi;
  assume that
A2: dom fi = A and
A3: for B st B in A holds fi.B = exp(1,B);
  per cases;
  case
    1 = {};
    hence thesis;
  end;
  case
    1 <> {};
    let A1,A2 be Ordinal such that
A4: A1 in 1 and
A5: 1 in A2;
    take B = {};
    thus B in dom fi by A1,A2,ORDINAL3:8;
    let D;
    assume that
    B c= D and
A6: D in dom fi;
    exp(1,D) = fi.D by A2,A3,A6;
    hence thesis by A4,A5,ORDINAL2:46;
  end;
end;

Lm8: for A st A <> {} & A is limit_ordinal holds ex fi st dom fi = A & (for B
st B in A holds fi.B = exp(C,B)) & ex D st D is_limes_of fi
proof
  defpred P[Ordinal] means $1 <> {} & $1 is limit_ordinal & for fi st dom fi =
  $1 & for B st B in $1 holds fi.B = exp(C,B) for D holds not D is_limes_of fi;
  let A such that
A1: A <> {} and
A2: A is limit_ordinal and
A3: for fi st dom fi = A & for B st B in A holds fi.B = exp(C,B) for D
  holds not D is_limes_of fi;
  deffunc F(Ordinal) = exp(C,$1);
A4: ex A st P[A] by A1,A2,A3;
  consider A such that
A5: P[A] and
A6: for A1 st P[A1] holds A c= A1 from ORDINAL1:sch 1(A4);
  consider fi such that
A7: dom fi = A & for B st B in A holds fi.B = F(B) from ORDINAL2:sch 3;
A8: now
    assume C = {} or C = 1;
    then {} is_limes_of fi or 1 is_limes_of fi by A5,A7,Lm6,Lm7;
    hence contradiction by A5,A7;
  end;
  then {} in C by ORDINAL3:8;
  then 1 c= C by Lm3,ORDINAL1:21;
  then
A9: 1 c< C by A8,XBOOLE_0:def 8;
A10: for B2,B1 being Ordinal st B1 in B2 & B2 in A holds exp(C,B1) in exp(C,
  B2)
  proof
    defpred V[Ordinal] means for B1 being Ordinal st B1 in $1 & $1 in A holds
    exp(C,B1) in exp(C,$1);
A11: V[B] implies V[succ B]
    proof
      assume
A12:  for B1 being Ordinal st B1 in B & B in A holds exp(C,B1) in exp (C,B);
      let B1 be Ordinal such that
A13:  B1 in succ B and
A14:  succ B in A;
A15:  B1 c= B by A13,ORDINAL1:22;
      B in succ B by ORDINAL1:6;
      then
A16:  B in A by A14,ORDINAL1:10;
A17:  1*^exp(C,B) = exp(C,B) by ORDINAL2:39;
A18:  exp(C,B) <> {}
      proof
        now
          per cases;
          suppose
            B = {};
            hence thesis by ORDINAL2:43;
          end;
          suppose
A19:        B <> {};
            B in succ B by ORDINAL1:6;
            then B in A by A14,ORDINAL1:10;
            hence thesis by A12,A19,ORDINAL3:8;
          end;
        end;
        hence thesis;
      end;
A20:  exp(C,succ B) = C*^exp(C,B) by ORDINAL2:44;
      then
A21:  exp(C,B) in exp(C,succ B) by A9,A18,A17,ORDINAL1:11,ORDINAL2:40;
      now
        assume B1 <> B;
        then B1 c< B by A15,XBOOLE_0:def 8;
        then B1 in B by ORDINAL1:11;
        then exp(C,B1) in exp(C,B) by A12,A16;
        hence thesis by A21,ORDINAL1:10;
      end;
      hence thesis by A9,A18,A20,A17,ORDINAL1:11,ORDINAL2:40;
    end;
A22: for B st B <> {} & B is limit_ordinal & for D st D in B holds V[D]
    holds V[B]
    proof
      let B such that
A23:  B <> {} and
A24:  B is limit_ordinal and
A25:  for D st D in B holds V[D];
      let B1 be Ordinal;
      assume that
A26:  B1 in B and
A27:  B in A;
      consider psi such that
A28:  dom psi = B and
A29:  for D st D in B holds psi.D = exp(C,D) and
      ex D st D is_limes_of psi by A6,A24,A26,A27,ORDINAL1:5;
      psi.B1 = exp(C,B1) by A26,A29;
      then
A30:  exp(C,B1) in rng psi by A26,A28,FUNCT_1:def 3;
      psi is increasing
      proof
        let B1,B2 be Ordinal;
        assume that
A31:    B1 in B2 and
A32:    B2 in dom psi;
        B2 in A by A27,A28,A32,ORDINAL1:10;
        then
A33:    exp(C,B1) in exp(C,B2) by A25,A28,A31,A32;
        psi.B1 = exp(C,B1) by A28,A29,A31,A32,ORDINAL1:10;
        hence thesis by A28,A29,A32,A33;
      end;
      then
A34:  lim psi = sup psi by A23,A24,A28,Th8;
      exp(C,B) = lim psi by A23,A24,A28,A29,ORDINAL2:45;
      hence thesis by A34,A30,ORDINAL2:19;
    end;
A35: V[{}];
    thus for B holds V[B] from ORDINAL2:sch 1(A35,A11,A22);
  end;
  fi is increasing
  proof
    let B1,B2 be Ordinal;
    assume that
A36: B1 in B2 and
A37: B2 in dom fi;
A38: fi.B1 = exp(C,B1) by A7,A36,A37,ORDINAL1:10;
    exp(C,B1) in exp(C,B2) by A7,A10,A36,A37;
    hence thesis by A7,A37,A38;
  end;
  then sup fi is_limes_of fi by A5,A7,Th8;
  hence contradiction by A5,A7;
end;

theorem Th21:
  A <> {} & A is limit_ordinal implies for fi st dom fi = A & for
  B st B in A holds fi.B = exp(C,B) holds exp(C,A) is_limes_of fi
proof
  assume that
A1: A <> {} and
A2: A is limit_ordinal;
  consider psi such that
A3: dom psi = A and
A4: for B st B in A holds psi.B = exp(C,B) and
A5: ex D st D is_limes_of psi by A1,A2,Lm8;
  let fi such that
A6: dom fi = A and
A7: for B st B in A holds fi.B = exp(C,B);
  now
    let x;
    assume
A8: x in A;
    then reconsider B = x as Ordinal;
    thus fi.x = exp(C,B) by A7,A8
      .= psi.x by A4,A8;
  end;
  then fi = psi by A6,A3,FUNCT_1:2;
  then consider D such that
A9: D is_limes_of fi by A5;
  D = lim fi by A9,ORDINAL2:def 10
    .= exp(C,A) by A1,A2,A6,A7,ORDINAL2:45;
  hence thesis by A9;
end;

theorem Th22:
  C <> {} implies exp(C,A) <> {}
proof
  defpred P[Ordinal] means exp(C,$1) <> {};
  assume
A1: C <> {};
A2: for A st P[A] holds P[succ A]
  proof
    let A such that
A3: exp(C,A) <> {};
    exp(C,succ A) = C*^exp(C,A) by ORDINAL2:44;
    hence thesis by A1,A3,ORDINAL3:31;
  end;
A4: for A st A <> {} & A is limit_ordinal & for B st B in A holds P[B] holds
  P[A]
  proof
    let A such that
A5: A <> {} and
A6: A is limit_ordinal and
A7: for B st B in A holds exp(C,B) <> {};
    consider fi such that
A8: dom fi = A and
A9: for B st B in A holds fi.B = exp(C,B) and
A10: ex D st D is_limes_of fi by A5,A6,Lm8;
A11: exp(C,A) = lim fi by A5,A6,A8,A9,ORDINAL2:45;
    assume
A12: exp(C,A) = {};
    consider D such that
A13: D is_limes_of fi by A10;
    lim fi = D by A13,ORDINAL2:def 10;
    then consider B such that
A14: B in dom fi and
A15: for D st B c= D & D in dom fi holds fi.D = {} by A11,A13,A12,
ORDINAL2:def 9;
    fi.B = exp(C,B) by A8,A9,A14;
    hence contradiction by A7,A8,A14,A15;
  end;
A16: P[{}] by ORDINAL2:43;
  for A holds P[A] from ORDINAL2:sch 1(A16,A2,A4);
  hence thesis;
end;

theorem Th23:
  1 in C implies exp(C,A) in exp(C,succ A)
proof
A1: 1*^exp(C,A) = exp(C,A) by ORDINAL2:39;
  assume 1 in C;
  then exp(C,A) in C*^exp(C,A) by A1,Th22,ORDINAL2:40;
  hence thesis by ORDINAL2:44;
end;

theorem Th24:
  1 in C & A in B implies exp(C,A) in exp(C,B)
proof
  defpred OO[Ordinal] means for A st A in $1 holds exp(C,A) in exp(C,$1);
A1: for B st B <> {} & B is limit_ordinal & for D st D in B holds OO[D]
  holds OO[B]
  proof
    deffunc F(Ordinal) = exp(C,$1);
    let B such that
A2: B <> {} and
A3: B is limit_ordinal and
A4: for D st D in B holds OO[D];
    consider fi such that
A5: dom fi = B & for D st D in B holds fi.D = F(D) from ORDINAL2:sch
    3;
    fi is increasing
    proof
      let B1,B2 be Ordinal;
      assume that
A6:   B1 in B2 and
A7:   B2 in dom fi;
A8:   fi.B1 = exp(C,B1) by A5,A6,A7,ORDINAL1:10;
      exp(C,B1) in exp(C,B2) by A4,A5,A6,A7;
      hence thesis by A5,A7,A8;
    end;
    then
A9: sup fi = lim fi by A2,A3,A5,Th8;
    let A such that
A10: A in B;
    fi.A = exp(C,A) by A10,A5;
    then
A11: exp(C,A) in rng fi by A10,A5,FUNCT_1:def 3;
    exp(C,B) = lim fi by A2,A3,A5,ORDINAL2:45;
    hence thesis by A9,A11,ORDINAL2:19;
  end;
  assume
A12: 1 in C;
A13: for B st OO[B] holds OO[succ B]
  proof
    let B such that
A14: for A st A in B holds exp(C,A) in exp(C,B);
    let A;
    assume A in succ B;
    then
A15: A c= B by ORDINAL1:22;
A16: now
      assume A <> B;
      then A c< B by A15,XBOOLE_0:def 8;
      hence exp(C,A) in exp(C,B) by A14,ORDINAL1:11;
    end;
    exp(C,B) in exp(C,succ B) by A12,Th23;
    hence thesis by A16,ORDINAL1:10;
  end;
A17: OO[{}];
  for B holds OO[B] from ORDINAL2:sch 1(A17,A13,A1);
  hence thesis;
end;

theorem Th25:
  1 in C & (for A st A in dom fi holds fi.A = exp(C,A)) implies fi
  is increasing
proof
  assume that
A1: 1 in C and
A2: for A st A in dom fi holds fi.A = exp(C,A);
  let A,B;
  assume that
A3: A in B and
A4: B in dom fi;
A5: fi.B = exp(C,B) by A2,A4;
  fi.A = exp(C,A) by A2,A3,A4,ORDINAL1:10;
  hence thesis by A1,A3,A5,Th24;
end;

theorem
  1 in C & A <> {} & A is limit_ordinal implies for fi st dom fi = A &
  for B st B in A holds fi.B = exp(C,B) holds exp(C,A) = sup fi
proof
  assume that
A1: 1 in C and
A2: A <> {} and
A3: A is limit_ordinal;
  let fi;
  assume that
A4: dom fi = A and
A5: for B st B in A holds fi.B = exp(C,B);
  fi is increasing by A1,A4,A5,Th25;
  then lim fi = sup fi by A2,A3,A4,Th8;
  hence thesis by A2,A3,A4,A5,ORDINAL2:45;
end;

theorem
  C <> {} & A c= B implies exp(C,A) c= exp(C,B)
proof
A1: A c< B iff A c= B & A <> B by XBOOLE_0:def 8;
  assume C <> {};
  then {} in C by ORDINAL3:8;
  then
A2: 1 c= C by Lm3,ORDINAL1:21;
  assume A c= B;
  then
A3: A in B or A = B by A1,ORDINAL1:11;
  now
    per cases;
    suppose
A4:   C = 1;
      then exp(C,A) = 1 by ORDINAL2:46;
      hence thesis by A4,ORDINAL2:46;
    end;
    suppose
      C <> 1;
      then 1 c< C by A2,XBOOLE_0:def 8;
      then 1 in C by ORDINAL1:11;
      then exp(C,A) in exp(C,B) or exp(C,A) = exp(C,B) by A3,Th24;
      hence thesis by ORDINAL1:def 2;
    end;
  end;
  hence thesis;
end;

theorem
  A c= B implies exp(A,C) c= exp(B,C)
proof
  defpred P[Ordinal] means exp(A,$1) c= exp(B,$1);
  assume
A1: A c= B;
A2: for C st P[C] holds P[succ C]
  proof
    let C;
A3: exp(B,succ C) = B*^exp(B,C) by ORDINAL2:44;
    exp(A,succ C) = A*^exp(A,C) by ORDINAL2:44;
    hence thesis by A1,A3,ORDINAL3:20;
  end;
A4: for C st C <> {} & C is limit_ordinal & for D st D in C holds P[D] holds
  P[C]
  proof
    deffunc F(Ordinal) = exp(A,$1);
    let C;
    assume that
A5: C <> {} and
A6: C is limit_ordinal and
A7: for D st D in C holds exp(A,D) c= exp(B,D);
    consider f1 such that
A8: dom f1 = C & for D st D in C holds f1.D = F(D) from ORDINAL2:sch
    3;
    deffunc F(Ordinal) = exp(B,$1);
    consider f2 such that
A9: dom f2 = C & for D st D in C holds f2.D = F(D) from ORDINAL2:sch
    3;
A10: now
      let D;
      assume
A11:  D in dom f1;
      then
A12:  f1.D = exp(A,D) by A8;
      f2.D = exp(B,D) by A8,A9,A11;
      hence f1.D c= f2.D by A7,A8,A11,A12;
    end;
A13: exp(A,C) is_limes_of f1 by A5,A6,A8,Th21;
    exp(B,C) is_limes_of f2 by A5,A6,A9,Th21;
    hence thesis by A8,A9,A13,A10,Th6;
  end;
  exp(A,{}) = 1 by ORDINAL2:43;
  then
A14: P[{}] by ORDINAL2:43;
  for C holds P[C] from ORDINAL2:sch 1(A14,A2,A4);
  hence thesis;
end;

theorem
  1 in C & A <> {} implies 1 in exp(C,A)
proof
  assume that
A1: 1 in C and
A2: A <> {};
  exp(C,{}) = 1 by ORDINAL2:43;
  hence thesis by A1,A2,Th24,ORDINAL3:8;
end;

theorem Th30:
  exp(C,A+^B) = exp(C,B)*^exp(C,A)
proof
  defpred P[Ordinal] means exp(C,A+^$1) = exp(C,$1)*^exp(C,A);
A1: 1 = exp(C,{}) by ORDINAL2:43;
A2: for B st P[B] holds P[succ B]
  proof
    let B such that
A3: exp(C,A+^B) = exp(C,B)*^exp(C,A);
    thus exp(C,A+^succ B) = exp(C,succ(A+^B)) by ORDINAL2:28
      .= C*^exp(C,A+^B) by ORDINAL2:44
      .= C*^exp(C,B)*^exp(C,A) by A3,ORDINAL3:50
      .= exp(C,succ B)*^exp(C,A) by ORDINAL2:44;
  end;
A4: for B st B <> {} & B is limit_ordinal & for D st D in B holds P[D] holds
  P[B]
  proof
    deffunc F(Ordinal) = exp(C,$1);
    let B such that
A5: B <> {} and
A6: B is limit_ordinal and
A7: for D st D in B holds exp(C,A+^D) = exp(C,D)*^exp(C,A);
    consider fi such that
A8: dom fi = B & for D st D in B holds fi.D = F(D) from ORDINAL2:sch
    3;
    consider psi such that
A9: dom psi = A+^B & for D st D in A+^B holds psi.D = F(D) from
    ORDINAL2:sch 3;
    deffunc F(Ordinal) = exp(C,$1);
    consider f1 such that
A10: dom f1 = A & for D st D in A holds f1.D = F(D) from ORDINAL2:sch
    3;
A11: now
      let D;
      assume D in dom(fi*^exp(C,A));
      then
A12:  D in dom fi by ORDINAL3:def 4;
      hence psi.((dom f1)+^D) = exp(C,A+^D) by A8,A9,A10,ORDINAL2:32
        .= (exp(C,D))*^exp(C,A) by A7,A8,A12
        .= (fi.D)*^exp(C,A) by A8,A12
        .= (fi*^exp(C,A)).D by A12,ORDINAL3:def 4;
    end;
A13: now
      let D such that
A14:  D in dom f1;
      A c= A+^B by ORDINAL3:24;
      hence psi.D = exp(C,D) by A9,A10,A14
        .= f1.D by A10,A14;
    end;
    dom psi = (dom f1)+^(dom(fi*^exp(C,A))) by A8,A9,A10,ORDINAL3:def 4;
    then
A15: psi = f1^(fi*^exp(C,A)) by A13,A11,Def1;
    exp(C,B)*^exp(C,A) is_limes_of fi*^exp(C,A) by A5,A6,A8,Th5,Th21;
    then
A16: exp(C,B)*^exp(C,A) is_limes_of psi by A15,Th3;
A17: A+^B <> {} by A5,ORDINAL3:26;
    A+^B is limit_ordinal by A5,A6,ORDINAL3:29;
    then lim psi = exp(C,A+^B) by A9,A17,ORDINAL2:45;
    hence thesis by A16,ORDINAL2:def 10;
  end;
  exp(C,A) = 1*^exp(C,A) by ORDINAL2:39;
  then
A18: P[{}] by A1,ORDINAL2:27;
  for B holds P[B] from ORDINAL2:sch 1(A18,A2,A4);
  hence thesis;
end;

theorem
  exp(exp(C,A),B) = exp(C,B*^A)
proof
  defpred P[Ordinal] means exp(exp(C,A),$1) = exp(C,$1*^A);
A1: exp(C,{}) = 1 by ORDINAL2:43;
A2: for B st P[B] holds P[succ B]
  proof
    let B;
    assume exp(exp(C,A),B) = exp(C,B*^A);
    hence exp(exp(C,A),succ B) = exp(C,A)*^exp(C,B*^A) by ORDINAL2:44
      .= exp(C,B*^A+^A) by Th30
      .= exp(C,(succ B)*^A) by ORDINAL2:36;
  end;
A3: for B st B <> {} & B is limit_ordinal & for D st D in B holds P[D] holds
  P[B]
  proof
    deffunc F(Ordinal) = exp(exp(C,A),$1);
    let B;
    assume that
A4: B <> {} and
A5: B is limit_ordinal and
A6: for D st D in B holds exp(exp(C,A),D) = exp(C,D*^A);
    consider fi such that
A7: dom fi = B & for D st D in B holds fi.D = F(D) from ORDINAL2:sch
    3;
    deffunc F(Ordinal) = $1*^A;
    consider f1 such that
A8: dom f1 = B & for D st D in B holds f1.D = F(D) from ORDINAL2:sch
    3;
    deffunc F(Ordinal) = exp(C,$1);
    consider f2 such that
A9: dom f2 = B*^A & for D st D in B*^A holds f2.D = F(D) from
    ORDINAL2:sch 3;
A10: now
      assume
A11:  A <> {};
      then B*^A <> {} by A4,ORDINAL3:31;
      then
A12:  exp(C,B*^A) is_limes_of f2 by A5,A9,Th21,ORDINAL3:40;
A13:  rng f1 c= dom f2
      proof
        let x;
        assume x in rng f1;
        then consider y such that
A14:    y in dom f1 and
A15:    x = f1.y by FUNCT_1:def 3;
        reconsider y as Ordinal by A14;
        x = y*^A by A8,A14,A15;
        hence thesis by A8,A9,A11,A14,ORDINAL2:40;
      end;
A16:  sup rng f1 = dom f2
      proof
        sup rng f1 c= sup dom f2 by A13,ORDINAL2:22;
        hence sup rng f1 c= dom f2 by ORDINAL2:18;
        let x;
        assume
A17:    x in dom f2;
        then reconsider D = x as Ordinal;
        consider A1 such that
A18:    A1 in B and
A19:    D in A1*^A by A5,A9,A17,ORDINAL3:41;
        f1.A1 = A1*^A by A8,A18;
        then A1*^A in rng f1 by A8,A18,FUNCT_1:def 3;
        then A1*^A in sup rng f1 by ORDINAL2:19;
        hence thesis by A19,ORDINAL1:10;
      end;
A20:  dom(f2*f1) = B
      proof
        thus dom(f2*f1) c= B by A8,RELAT_1:25;
        let x;
        assume
A21:    x in B;
        then reconsider E = x as Ordinal;
A22:    f1.E = E*^A by A8,A21;
        E*^A in B*^A by A11,A21,ORDINAL2:40;
        hence thesis by A8,A9,A21,A22,FUNCT_1:11;
      end;
      now
        let x;
        assume
A23:    x in B;
        then reconsider D = x as Ordinal;
A24:    f1.D = D*^A by A8,A23;
        thus fi.x = exp(exp(C,A),D) by A7,A23
          .= exp(C,D*^A) by A6,A23
          .= f2.(f1.D) by A9,A11,A23,A24,ORDINAL2:40
          .= (f2*f1).x by A8,A23,FUNCT_1:13;
      end;
      then fi = f2*f1 by A7,A20,FUNCT_1:2;
      then exp(C,B*^A) is_limes_of fi by A8,A11,A12,A16,Th14,Th19;
      then exp(C,B*^A) = lim fi by ORDINAL2:def 10;
      hence thesis by A4,A5,A7,ORDINAL2:45;
    end;
A25: B*^{} = {} by ORDINAL2:38;
    exp(C,{}) = 1 by ORDINAL2:43;
    hence thesis by A25,A10,ORDINAL2:46;
  end;
  exp(exp(C,A),{}) = 1 by ORDINAL2:43;
  then
A26: P[{}] by A1,ORDINAL2:35;
  for B holds P[B] from ORDINAL2:sch 1(A26,A2,A3);
  hence thesis;
end;

theorem
  1 in C implies A c= exp(C,A)
proof
  defpred P[Ordinal] means $1 c= exp(C,$1);
  assume
A1: 1 in C;
A2: P[B] implies P[succ B]
  proof
    assume
A3: B c= exp(C,B);
A4: exp(C,B) = 1*^exp(C,B) by ORDINAL2:39;
    exp(C,succ B) = C*^exp(C,B) by ORDINAL2:44;
    then exp(C,B) in exp(C,succ B) by A1,A4,Th22,ORDINAL2:40;
    then B in exp(C,succ B) by A3,ORDINAL1:12;
    hence thesis by ORDINAL1:21;
  end;
A5: for A st A <> {} & A is limit_ordinal & for B st B in A holds P[B] holds
  P[A]
  proof
    deffunc F(Ordinal) = exp(C,$1);
    let A such that
A6: A <> {} and
A7: A is limit_ordinal and
A8: for B st B in A holds B c= exp(C,B);
    consider fi such that
A9: dom fi = A & for B st B in A holds fi.B = F(B) from ORDINAL2:sch
    3;
    let x;
    assume
A10: x in A;
    then reconsider B = x as Ordinal;
    fi.B = exp(C,B) by A9,A10;
    then exp(C,B) in rng fi by A9,A10,FUNCT_1:def 3;
    then
A11: exp(C,B) in sup fi by ORDINAL2:19;
    fi is increasing by A1,A9,Th25;
    then
A12: sup fi = lim fi by A6,A7,A9,Th8
      .= exp(C,A) by A6,A7,A9,ORDINAL2:45;
    B c= exp(C,B) by A8,A10;
    hence thesis by A12,A11,ORDINAL1:12;
  end;
A13: P[{}] by XBOOLE_1:2;
  P[B] from ORDINAL2:sch 1(A13,A2,A5);
  hence thesis;
end;

::$N Fixed-point lemma for normal functions
scheme
  CriticalNumber { phi(Ordinal) -> Ordinal } : ex A st phi(A) = A
provided
A1: for A,B st A in B holds phi(A) in phi(B) and
A2: for A st A <> {} & A is limit_ordinal for phi st dom phi = A & for B
st B in A holds phi.B = phi(B) holds phi(A) is_limes_of phi
proof
A3: now
    defpred P[Ordinal] means not $1 c= phi($1);
    assume
A4: ex A st P[A];
    consider A such that
A5: P[A] and
A6: for B st P[B] holds A c= B from ORDINAL1:sch 1(A4);
    phi(phi(A)) in phi(A) by A1,A5,ORDINAL1:16;
    then not phi(A) c= phi(phi(A)) by ORDINAL1:5;
    hence contradiction by A5,A6;
  end;
  deffunc G(Ordinal,T-Sequence) = {};
  deffunc F(Ordinal,Ordinal) = phi($2);
  consider phi such that
A7: dom phi = omega and
A8: {} in omega implies phi.{} = phi({}) and
A9: for A st succ A in omega holds phi.(succ A) = F(A,phi.A) and
  for A st A in omega & A <> {} & A is limit_ordinal holds phi.A = G(A,phi
  |A) from ORDINAL2:sch 11;
  assume
A10: not thesis;
A11: now
    let A;
A12: A <> phi(A) by A10;
    A c= phi(A) by A3;
    then A c< phi(A) by A12,XBOOLE_0:def 8;
    hence A in phi(A) by ORDINAL1:11;
  end;
A13: phi is increasing
  proof
    let A,B;
    assume that
A14: A in B and
A15: B in dom phi;
    defpred R[Ordinal] means A+^$1 in omega & $1 <> {} implies phi.A in phi.(A
    +^$1);
A16: for B st B <> {} & B is limit_ordinal & for C st C in B holds R[C]
    holds R[B]
    proof
      let B such that
A17:  B <> {} and
A18:  B is limit_ordinal and
      for C st C in B holds A+^C in omega & C <> {} implies phi.A in phi.(
      A+^C) and
A19:  A+^B in omega and
A20:  B <> {};
      A+^B <> {} by A20,ORDINAL3:26;
      then
A21:  {} in A+^B by ORDINAL3:8;
      A+^B is limit_ordinal by A17,A18,ORDINAL3:29;
      then omega c= A+^B by A21,ORDINAL1:def 11;
      hence thesis by A19,ORDINAL1:5;
    end;
A22: for C st R[C] holds R[succ C]
    proof
      let C such that
A23:  A+^C in omega & C <> {} implies phi.A in phi.(A+^C) and
A24:  A+^succ C in omega and
      succ C <> {};
      reconsider D = phi.(A+^C) as Ordinal;
A25:  A+^C in succ(A+^C) by ORDINAL1:6;
A26:  D in phi(D) by A11;
A27:  A+^succ C = succ(A+^C) by ORDINAL2:28;
      then phi.(A+^succ C) = phi(D) by A9,A24;
      hence thesis by A23,A24,A25,A27,A26,ORDINAL1:10,ORDINAL2:27;
    end;
A28: R[{}];
A29: for C holds R[C] from ORDINAL2:sch 1(A28,A22,A16);
    ex C st B = A+^C & C <> {} by A14,ORDINAL3:28;
    hence thesis by A7,A15,A29;
  end;
  deffunc phi(Ordinal) = phi ($1);
  consider fi such that
A30: dom fi = sup phi & for A st A in sup phi holds fi.A = phi(A) from
  ORDINAL2:sch 3;
  phi({}) in rng phi by A7,A8,Lm1,FUNCT_1:def 3;
  then
A31: sup phi <> {} by ORDINAL2:19;
  then
A32: phi(sup phi) is_limes_of fi by A2,A7,A13,A30,Lm2,Th16;
A33: sup fi c= sup phi
  proof
    let x;
    assume
A34: x in sup fi;
    then reconsider A = x as Ordinal;
    consider B such that
A35: B in rng fi and
A36: A c= B by A34,ORDINAL2:21;
    consider y such that
A37: y in dom fi and
A38: B = fi.y by A35,FUNCT_1:def 3;
    reconsider y as Ordinal by A37;
    consider C such that
A39: C in rng phi and
A40: y c= C by A30,A37,ORDINAL2:21;
    y c< C iff y <> C & y c= C by XBOOLE_0:def 8;
    then
A41: phi(y) in phi(C) or y = C by A1,A40,ORDINAL1:11;
    B = phi(y) by A30,A37,A38;
    then
A42: B c= phi(C) by A41,ORDINAL1:def 2;
    consider z such that
A43: z in dom phi and
A44: C = phi.z by A39,FUNCT_1:def 3;
    reconsider z as Ordinal by A43;
A45: succ z in omega by A7,A43,Lm2,ORDINAL1:28;
    then
A46: phi.succ z in rng phi by A7,FUNCT_1:def 3;
    phi.succ z = phi(C) by A9,A44,A45;
    then phi(C) in sup phi by A46,ORDINAL2:19;
    then B in sup phi by A42,ORDINAL1:12;
    hence thesis by A36,ORDINAL1:12;
  end;
A47: fi is increasing
  proof
    let A,B;
    assume that
A48: A in B and
A49: B in dom fi;
A50: fi.B = phi(B) by A30,A49;
    fi.A = phi(A) by A30,A48,A49,ORDINAL1:10;
    hence thesis by A1,A48,A50;
  end;
  sup phi is limit_ordinal by A7,A13,Lm2,Th16;
  then sup fi = lim fi by A30,A31,A47,Th8
    .= phi(sup phi) by A32,ORDINAL2:def 10;
  hence contradiction by A11,A33,ORDINAL1:5;
end;

reserve W for Universe;

registration
  let W;
  cluster ordinal for Element of W;
  existence
  proof
A1: On W c= W by ORDINAL2:7;
    {} in On W by CLASSES2:51,ORDINAL3:8;
    hence thesis by A1;
  end;
end;

definition
  let W;
  mode Ordinal of W is ordinal Element of W;
  mode Ordinal-Sequence of W is Function of On W, On W;
end;

registration
  let W;
  cluster non empty for Ordinal of W;
  existence
  proof
A1: On W c= W by ORDINAL2:7;
    {} in On W by CLASSES2:51,ORDINAL3:8;
    then 1 in W by A1,Lm3,CLASSES2:5;
    hence thesis;
  end;
end;

registration
  let W;
  cluster On W -> non empty;
  coherence by CLASSES2:51;
end;

registration
  let W;
  cluster -> T-Sequence-like Ordinal-yielding for Ordinal-Sequence of W;
  coherence
  proof
    let s be Ordinal-Sequence of W;
    thus dom s is ordinal by FUNCT_2:def 1;
    take On W;
    thus rng s c= On W by RELAT_1:def 19;
  end;
end;

reserve A1,B1 for Ordinal of W,
  phi for Ordinal-Sequence of W;

scheme
  UOSLambda { W() -> Universe, F(set) -> Ordinal of W() } : ex phi being
Ordinal-Sequence of W() st for a being Ordinal of W() holds phi.a = F(a) proof
  consider psi such that
A1: dom psi = On W() & for A st A in On W() holds psi.A = F(A) from
  ORDINAL2:sch 3;
  rng psi c= On W()
  proof
    let x;
    assume x in rng psi;
    then consider y such that
A2: y in dom psi and
A3: x = psi.y by FUNCT_1:def 3;
    reconsider y as Ordinal by A2;
    x = F(y) by A1,A2,A3;
    hence thesis by ORDINAL1:def 9;
  end;
  then reconsider psi as Ordinal-Sequence of W() by A1,FUNCT_2:def 1,RELSET_1:4
;
  take psi;
  let a be Ordinal of W();
  a in On W() by ORDINAL1:def 9;
  hence thesis by A1;
end;

definition
  let W;

  func 0-element_of W -> Ordinal of W equals
  {};
  correctness
  proof
A1: On W c= W by ORDINAL2:7;
    {} in On W by ORDINAL3:8;
    then reconsider A = {} as Ordinal of W by A1;
    A = {};
    hence thesis;
  end;
  func 1-element_of W -> non empty Ordinal of W equals
  1;
  correctness
  proof
A2: On W c= W by ORDINAL2:7;
    {} in On W by ORDINAL3:8;
    then reconsider A = 1 as Ordinal of W by A2,Lm3,CLASSES2:5;
    A = 1;
    hence thesis;
  end;
  let phi,A1;
  redefine func phi.A1 -> Ordinal of W;
  coherence
  proof
    reconsider B = phi.A1 as Ordinal;
A3: dom phi = On W by FUNCT_2:def 1;
A4: rng phi c= On W by RELAT_1:def 19;
    A1 in On W by ORDINAL1:def 9;
    then B in rng phi by A3,FUNCT_1:def 3;
    then
A5: B in On W by A4;
    On W c= W by ORDINAL2:7;
    hence thesis by A5;
  end;
end;

definition
  let W;
  let p2,p1 be Ordinal-Sequence of W;
  redefine func p1*p2 -> Ordinal-Sequence of W;
  coherence
  proof
A1: rng p2 c= On W by RELAT_1:def 19;
A2: dom p2 = On W by FUNCT_2:def 1;
    dom p1 = On W by FUNCT_2:def 1;
    then
A3: dom(p1*p2) = On W by A2,A1,RELAT_1:27;
    then reconsider f = p1*p2 as T-Sequence by ORDINAL1:def 7;
A4: rng p1 c= On W by RELAT_1:def 19;
    rng(p1*p2) c= rng p1 by RELAT_1:26;
    then rng f c= On W by A4,XBOOLE_1:1;
    hence thesis by A3,FUNCT_2:def 1,RELSET_1:4;
  end;
end;

theorem
  0-element_of W = {} & 1-element_of W = 1;

definition
  let W,A1;
  redefine func succ A1 -> non empty Ordinal of W;
  coherence by CLASSES2:5;
  let B1;
  redefine func A1 +^ B1 -> Ordinal of W;
  coherence
  proof
    defpred P[Ordinal] means $1 in W implies A1+^$1 in W;
A1: for B st for C st C in B holds P[C] holds P[B]
    proof
      let B such that
A2:   for C st C in B holds C in W implies A1+^C in W and
A3:   B in W;
      [:B,{1-element_of W}:] in W by A3,CLASSES2:61;
      then [:A1,{0-element_of W}:] \/ [:B,{1-element_of W}:] in W by
CLASSES2:60;
      then
A4:   card([:A1,{0-element_of W}:] \/ [:B,{1-element_of W}:]) in card W by
CLASSES2:1;
A5:   A1+^B c= W
      proof
        let x;
        assume
A6:     x in A1+^B;
        then reconsider A = x as Ordinal;
A7:     now
A8:       B c= W by A3,ORDINAL1:def 2;
          assume A1 c= A;
          then consider C such that
A9:       A = A1+^C by ORDINAL3:27;
          C in B by A6,A9,ORDINAL3:22;
          hence thesis by A2,A9,A8;
        end;
A10:    A in A1 or A1 c= A by ORDINAL1:16;
        A1 c= W by ORDINAL1:def 2;
        hence thesis by A10,A7;
      end;
      card(A1+^B) = card([:A1,{0-element_of W}:] \/ [:B,{ 1-element_of W}
      :] ) by CARD_2:9;
      hence thesis by A4,A5,CLASSES1:1;
    end;
    for B holds P[B] from ORDINAL1:sch 2(A1);
    hence thesis;
  end;
end;

definition
  let W,A1,B1;
  redefine func A1 *^ B1 -> Ordinal of W;
  coherence
  proof
    defpred P[Ordinal] means $1 in W implies $1*^B1 in W;
A1: for A st for C st C in A holds P[C] holds P[A]
    proof
      let A such that
A2:   for C st C in A holds C in W implies C*^B1 in W and
A3:   A in W;
      [:A,B1:] in W by A3,CLASSES2:61;
      then
A4:   card [:A,B1:] in card W by CLASSES2:1;
A5:   A*^B1 c= W
      proof
        let x;
A6:     B1 c= W by ORDINAL1:def 2;
        assume
A7:     x in A*^B1;
        then reconsider B = x as Ordinal;
        B1 <> {} by A7,ORDINAL2:38;
        then consider C,D such that
A8:     B = C*^B1+^D and
A9:     D in B1 by ORDINAL3:47;
        C*^B1 c= B by A8,ORDINAL3:24;
        then C*^B1 in A*^B1 by A7,ORDINAL1:12;
        then
A10:    C in A by ORDINAL3:34;
        A c= W by A3,ORDINAL1:def 2;
        then reconsider CB = C*^B1, D as Ordinal of W by A2,A9,A6,A10;
        x = CB+^D by A8;
        hence thesis;
      end;
      card(A*^B1) = card [:A,B1:] by CARD_2:11;
      hence thesis by A4,A5,CLASSES1:1;
    end;
    for A holds P[A] from ORDINAL1:sch 2(A1);
    hence thesis;
  end;
end;

theorem Th34:
  A1 in dom phi
proof
  dom phi = On W by FUNCT_2:def 1;
  hence thesis by ORDINAL1:def 9;
end;

theorem Th35:
  dom fi in W & rng fi c= W implies sup fi in W
proof
  assume that
A1: dom fi in W and
A2: rng fi c= W;
  ex A st rng fi c= A by ORDINAL2:def 4;
  then for x st x in rng fi holds x is Ordinal;
  then reconsider B = union rng fi as Ordinal by ORDINAL1:23;
A3: rng fi = fi.:(dom fi) by RELAT_1:113;
A4: sup fi c= succ B
  proof
    let x;
    assume
A5: x in sup fi;
    then reconsider A = x as Ordinal;
    consider C such that
A6: C in rng fi and
A7: A c= C by A5,ORDINAL2:21;
    C c= union rng fi by A6,ZFMISC_1:74;
    then A c= B by A7,XBOOLE_1:1;
    hence thesis by ORDINAL1:22;
  end;
  card dom fi in card W by A1,CLASSES2:1;
  then card rng fi in card W by A3,CARD_1:67,ORDINAL1:12;
  then rng fi in W by A2,CLASSES1:1;
  then union rng fi in W by CLASSES2:59;
  then succ B in W by CLASSES2:5;
  hence thesis by A4,CLASSES1:def 1;
end;

reserve L for T-Sequence;

theorem
  phi is increasing & phi is continuous & omega in W implies ex A st A
  in dom phi & phi.A = A
proof
  deffunc D(set,set) = {};
  assume that
A1: phi is increasing and
A2: phi is continuous and
A3: omega in W;
  deffunc C(set,set) = phi.$2;
  reconsider N = phi.(0-element_of W) as Ordinal;
  consider L such that
A4: dom L = omega and
A5: {} in omega implies L.{} = N and
A6: for A st succ A in omega holds L.(succ A) = C(A,L.A) and
  for A st A in omega & A <> {} & A is limit_ordinal holds L.A = D(A,L|A)
  from ORDINAL2:sch 5;
  defpred P[Ordinal] means $1 in dom L implies L.$1 is Ordinal of W;
A7: for A st P[A] holds P[succ A]
  proof
    let A such that
A8: A in dom L implies L.A is Ordinal of W and
A9: succ A in dom L;
    A in succ A by ORDINAL1:6;
    then reconsider x = L.A as Ordinal of W by A8,A9,ORDINAL1:10;
    L.succ A = phi.x by A4,A6,A9;
    hence thesis;
  end;
A10: for A st A <> {} & A is limit_ordinal & for B st B in A holds P[B]
  holds P[A]
  proof
    let A such that
A11: A <> {} and
A12: A is limit_ordinal and
    for B st B in A holds B in dom L implies L.B is Ordinal of W and
A13: A in dom L;
    {} in A by A11,ORDINAL3:8;
    then omega c= A by A12,ORDINAL1:def 11;
    hence thesis by A4,A13,ORDINAL1:5;
  end;
A14: P[{}] by A4,A5;
A15: for A holds P[A] from ORDINAL2:sch 1(A14,A7,A10);
  rng L c= sup rng L
  proof
    let x;
    assume
A16: x in rng L;
    then consider y such that
A17: y in dom L and
A18: x = L.y by FUNCT_1:def 3;
    reconsider y as Ordinal by A17;
    reconsider A = L.y as Ordinal of W by A15,A17;
    A in sup rng L by A16,A18,ORDINAL2:19;
    hence thesis by A18;
  end;
  then reconsider L as Ordinal-Sequence by ORDINAL2:def 4;
A19: dom phi = On W by FUNCT_2:def 1;
  assume
A20: not thesis;
A21: now
    let A1;
    A1 in dom phi by Th34;
    then
A22: A1 c= phi.A1 by A1,Th10;
    A1 <> phi.A1 by A20,Th34;
    then A1 c< phi.A1 by A22,XBOOLE_0:def 8;
    hence A1 in phi.A1 by ORDINAL1:11;
  end;
  L is increasing
  proof
    let A,B;
    assume that
A23: A in B and
A24: B in dom L;
    defpred P[Ordinal] means A+^$1 in omega & $1 <> {} implies L.A in L.(A+^$1
    );
A25: for B st B <> {} & B is limit_ordinal & for C st C in B holds P[C]
    holds P[B]
    proof
      let B such that
A26:  B <> {} and
A27:  B is limit_ordinal and
      for C st C in B holds A+^C in omega & C <> {} implies L.A in L.(A+^C
      ) and
A28:  A+^B in omega and
A29:  B <> {};
      A+^B <> {} by A29,ORDINAL3:26;
      then
A30:  {} in A+^B by ORDINAL3:8;
      A+^B is limit_ordinal by A26,A27,ORDINAL3:29;
      then omega c= A+^B by A30,ORDINAL1:def 11;
      hence thesis by A28,ORDINAL1:5;
    end;
A31: for C st P[C] holds P[succ C]
    proof
      let C such that
A32:  A+^C in omega & C <> {} implies L.A in L.(A+^C) and
A33:  A+^succ C in omega and
      succ C <> {};
A34:  A+^succ C = succ(A+^C) by ORDINAL2:28;
A35:  A+^C in succ(A+^C) by ORDINAL1:6;
      then reconsider D = L.(A+^C) as Ordinal of W by A4,A15,A33,A34,
ORDINAL1:10;
A36:  D in phi.D by A21;
      L.(A+^succ C) = phi.D by A6,A33,A34;
      hence thesis by A32,A33,A35,A34,A36,ORDINAL1:10,ORDINAL2:27;
    end;
A37: P[{}];
A38: for C holds P[C] from ORDINAL2:sch 1(A37,A31,A25);
    ex C st B = A+^C & C <> {} by A23,ORDINAL3:28;
    hence thesis by A4,A24,A38;
  end;
  then
A39: sup L is limit_ordinal by A4,Lm2,Th16;
A40: rng L c= W
  proof
    let x;
    assume x in rng L;
    then consider y such that
A41: y in dom L and
A42: x = L.y by FUNCT_1:def 3;
    reconsider y as Ordinal by A41;
    L.y is Ordinal of W by A15,A41;
    hence thesis by A42;
  end;
  then reconsider S = sup L as Ordinal of W by A3,A4,Th35;
  set fi = phi|sup L;
  N in rng L by A4,A5,Lm1,FUNCT_1:def 3;
  then
A43: sup L <> {} by ORDINAL2:19;
A44: S in On W by ORDINAL1:def 9;
  then
A45: phi.S is_limes_of fi by A2,A43,A39,A19,ORDINAL2:def 13;
  S c= dom phi by A44,A19,ORDINAL1:def 2;
  then
A46: dom fi = S by RELAT_1:62;
A47: sup fi c= sup L
  proof
    let x;
    assume
A48: x in sup fi;
    then reconsider A = x as Ordinal;
    consider B such that
A49: B in rng fi and
A50: A c= B by A48,ORDINAL2:21;
    consider y such that
A51: y in dom fi and
A52: B = fi.y by A49,FUNCT_1:def 3;
    reconsider y as Ordinal by A51;
    consider C such that
A53: C in rng L and
A54: y c= C by A46,A51,ORDINAL2:21;
    reconsider C1 = C as Ordinal of W by A40,A53;
    y c< C1 iff y c= C1 & y <> C1 by XBOOLE_0:def 8;
    then y in C1 & C1 in dom phi or y = C by A19,A54,ORDINAL1:11,def 9;
    then
A55: phi.y in phi.C1 or y = C1 by A1,ORDINAL2:def 12;
    B = phi.y by A51,A52,FUNCT_1:47;
    then
A56: B c= phi.C1 by A55,ORDINAL1:def 2;
    consider z such that
A57: z in dom L and
A58: C = L.z by A53,FUNCT_1:def 3;
    reconsider z as Ordinal by A57;
A59: succ z in omega by A4,A57,Lm2,ORDINAL1:28;
    then
A60: L.succ z in rng L by A4,FUNCT_1:def 3;
    L.succ z = phi.C by A6,A58,A59;
    then phi.C1 in sup L by A60,ORDINAL2:19;
    then B in sup L by A56,ORDINAL1:12;
    hence thesis by A50,ORDINAL1:12;
  end;
  fi is increasing
  proof
A61: dom fi c= dom phi by RELAT_1:60;
    let A,B;
    assume that
A62: A in B and
A63: B in dom fi;
A64: fi.B = phi.B by A63,FUNCT_1:47;
    fi.A = phi.A by A62,A63,FUNCT_1:47,ORDINAL1:10;
    hence thesis by A1,A62,A63,A61,A64,ORDINAL2:def 12;
  end;
  then sup fi = lim fi by A43,A39,A46,Th8
    .= phi.(sup L) by A45,ORDINAL2:def 10;
  then not S in phi.S by A47,ORDINAL1:5;
  hence contradiction by A21;
end;

begin :: Addenda
:: from ZFREFLE1, 2007.03.14, A.T.

reserve e,u for set;

theorem
  A is_cofinal_with B & B is_cofinal_with C implies A is_cofinal_with C
proof
  given xi1 being Ordinal-Sequence such that
A1: dom xi1 = B and
A2: rng xi1 c= A and
A3: xi1 is increasing and
A4: A = sup xi1;
  given xi2 being Ordinal-Sequence such that
A5: dom xi2 = C and
A6: rng xi2 c= B and
A7: xi2 is increasing and
A8: B = sup xi2;
  consider xi being Ordinal-Sequence such that
A9: xi = xi1*xi2 and
A10: xi is increasing by A3,A7,Th13;
  take xi;
  thus
A11: dom xi = C by A1,A5,A6,A9,RELAT_1:27;
  rng xi c= rng xi1 by A9,RELAT_1:26;
  hence
A12: rng xi c= A & xi is increasing by A2,A10,XBOOLE_1:1;
  thus A c= sup xi
  proof
    let a be set;
    assume
A13: a in A;
    then reconsider a as Ordinal;
    consider b being Ordinal such that
A14: b in rng xi1 and
A15: a c= b by A4,A13,ORDINAL2:21;
    consider e such that
A16: e in B and
A17: b = xi1.e by A1,A14,FUNCT_1:def 3;
    reconsider e as Ordinal by A16;
    consider c being Ordinal such that
A18: c in rng xi2 and
A19: e c= c by A8,A16,ORDINAL2:21;
    consider u such that
A20: u in C and
A21: c = xi2.u by A5,A18,FUNCT_1:def 3;
    reconsider u as Ordinal by A20;
A22: xi1.c = xi.u by A9,A11,A20,A21,FUNCT_1:12;
    xi.u in rng xi by A11,A20,FUNCT_1:def 3;
    then
A23: xi.u in sup xi by ORDINAL2:19;
    xi1.e c= xi1.c by A1,A3,A6,A18,A19,Th9;
    hence thesis by A15,A17,A22,A23,ORDINAL1:12,XBOOLE_1:1;
  end;
  sup rng xi c= sup A by A12,ORDINAL2:22;
  hence thesis by ORDINAL2:18;
end;

theorem
  A is_cofinal_with B implies (A is limit_ordinal iff B is limit_ordinal )
proof
  given psi such that
A1: dom psi = B and
A2: rng psi c= A and
A3: psi is increasing and
A4: A = sup psi;
  thus A is limit_ordinal implies B is limit_ordinal
  proof
    assume
A5: A is limit_ordinal;
    now
      let C;
      reconsider c = psi.C as Ordinal;
      assume
A6:   C in B;
      then psi.C in rng psi by A1,FUNCT_1:def 3;
      then succ c in A by A2,A5,ORDINAL1:28;
      then consider b being Ordinal such that
A7:   b in rng psi and
A8:   succ c c= b by A4,ORDINAL2:21;
      consider e such that
A9:   e in B and
A10:  b = psi.e by A1,A7,FUNCT_1:def 3;
      reconsider e as Ordinal by A9;
      c in succ c by ORDINAL1:6;
      then not e c= C by A1,A3,A6,A8,A10,Th9,ORDINAL1:5;
      then C in e by ORDINAL1:16;
      then succ C c= e by ORDINAL1:21;
      hence succ C in B by A9,ORDINAL1:12;
    end;
    hence thesis by ORDINAL1:28;
  end;
  thus thesis by A1,A3,A4,Th16;
end;

:: from 2009.09.28, A.T.

registration let D;
  let f,g be T-Sequence of D;
  cluster f^g -> D-valued;
  coherence
  proof
    rng f c= D & rng g c= D by RELAT_1:def 19;
    then
A1:  rng f \/ rng g c= D by XBOOLE_1:8;
    rng(f^g) c= rng f \/ rng g by Th2;
   hence rng(f^g) c= D by A1,XBOOLE_1:1;
  end;
end;