ordinal2.miz



    begin

    reserve A,A1,A2,B,C,D for Ordinal,

X,Y for set,

x,y,a,b,c for object,

L,L1,L2,L3 for Sequence,

f for Function;

    scheme :: ORDINAL2:sch1

    OrdinalInd { P[ Ordinal] } :

for A holds P[A]

      provided

       A1: P[ 0 ]

       and

       A2: for A st P[A] holds P[( succ A)]

       and

       A3: for A st A <> 0 & A is limit_ordinal & for B st B in A holds P[B] holds P[A];

      

       A4: for A st for B st B in A holds P[B] holds P[A]

      proof

        let A such that

         A5: for B st B in A holds P[B];

        

         A6: A <> 0 & (for B holds A <> ( succ B)) implies thesis by A3, A5, ORDINAL1: 29;

        now

          given B such that

           A7: A = ( succ B);

          B in A by A7, ORDINAL1: 6;

          hence thesis by A2, A5, A7;

        end;

        hence thesis by A1, A6;

      end;

      thus for A holds P[A] from ORDINAL1:sch 2( A4);

    end;

    theorem :: ORDINAL2:1

    

     Th1: A c= B iff ( succ A) c= ( succ B)

    proof

      A c= B iff A in ( succ B) by ORDINAL1: 22;

      hence thesis by ORDINAL1: 21;

    end;

    theorem :: ORDINAL2:2

    

     Th2: ( union ( succ A)) = A

    proof

      thus ( union ( succ A)) c= A

      proof

        let x be object;

        assume x in ( union ( succ A));

        then

        consider X such that

         A1: x in X and

         A2: X in ( succ A) by TARSKI:def 4;

        reconsider X as Ordinal by A2;

        X c= A by A2, ORDINAL1: 22;

        hence thesis by A1;

      end;

      thus thesis by ORDINAL1: 6, ZFMISC_1: 74;

    end;

    theorem :: ORDINAL2:3

    ( succ A) c= ( bool A)

    proof

      let x be object;

      assume

       A1: x in ( succ A);

      then

      reconsider B = x as Ordinal;

      x in A or x = A by A1, ORDINAL1: 8;

      then B c= A by ORDINAL1:def 2;

      hence thesis;

    end;

    theorem :: ORDINAL2:4

     0 is limit_ordinal by ZFMISC_1: 2;

    theorem :: ORDINAL2:5

    

     Th5: ( union A) c= A

    proof

      let x be object;

      assume x in ( union A);

      then

      consider Y such that

       A1: x in Y and

       A2: Y in A by TARSKI:def 4;

      Y c= A by A2, ORDINAL1:def 2;

      hence thesis by A1;

    end;

    definition

      let L;

      :: ORDINAL2:def1

      func last L -> set equals (L . ( union ( dom L)));

      coherence ;

    end

    theorem :: ORDINAL2:6

    ( dom L) = ( succ A) implies ( last L) = (L . A) by Th2;

    theorem :: ORDINAL2:7

    ( On X) c= X by ORDINAL1:def 9;

    theorem :: ORDINAL2:8

    

     Th8: ( On A) = A

    proof

      for x be object holds x in A iff x in A & x is Ordinal;

      hence thesis by ORDINAL1:def 9;

    end;

    theorem :: ORDINAL2:9

    

     Th9: X c= Y implies ( On X) c= ( On Y)

    proof

      assume

       A1: X c= Y;

      let x be object;

      assume x in ( On X);

      then x in X & x is Ordinal by ORDINAL1:def 9;

      hence thesis by A1, ORDINAL1:def 9;

    end;

    theorem :: ORDINAL2:10

    ( Lim X) c= X by ORDINAL1:def 10;

    theorem :: ORDINAL2:11

    X c= Y implies ( Lim X) c= ( Lim Y)

    proof

      assume

       A1: X c= Y;

      let x be object;

      assume x in ( Lim X);

      then x in X & ex A st x = A & A is limit_ordinal by ORDINAL1:def 10;

      hence thesis by A1, ORDINAL1:def 10;

    end;

    theorem :: ORDINAL2:12

    ( Lim X) c= ( On X)

    proof

      let x be object;

      assume x in ( Lim X);

      then x in X & ex A st x = A & A is limit_ordinal by ORDINAL1:def 10;

      hence thesis by ORDINAL1:def 9;

    end;

    theorem :: ORDINAL2:13

    

     Th13: (for x st x in X holds x is Ordinal) implies ( meet X) is Ordinal

    proof

      assume

       A1: for x st x in X holds x is Ordinal;

      now

        defpred P[ Ordinal] means $1 in X;

        set x = the Element of X;

        assume

         A2: X <> 0 ;

        then x is Ordinal by A1;

        then

         A3: ex A st P[A] by A2;

        consider A such that

         A4: P[A] & for B st P[B] holds A c= B from ORDINAL1:sch 1( A3);

        for x be object holds x in A iff for Y st Y in X holds x in Y

        proof

          let x be object;

          thus x in A implies for Y st Y in X holds x in Y

          proof

            assume

             A5: x in A;

            let Y;

            assume

             A6: Y in X;

            then

            reconsider B = Y as Ordinal by A1;

            A c= B by A4, A6;

            hence thesis by A5;

          end;

          assume for Y st Y in X holds x in Y;

          hence thesis by A4;

        end;

        hence thesis by A2, SETFAM_1:def 1;

      end;

      hence thesis by SETFAM_1:def 1;

    end;

    registration

      cluster limit_ordinal for Ordinal;

      existence

      proof

        take omega ;

        thus thesis by ORDINAL1:def 11;

      end;

    end

    definition

      let X;

      :: ORDINAL2:def2

      func inf X -> Ordinal equals ( meet ( On X));

      coherence

      proof

        x in ( On X) implies x is Ordinal by ORDINAL1:def 9;

        hence thesis by Th13;

      end;

      :: ORDINAL2:def3

      func sup X -> Ordinal means

      : Def3: ( On X) c= it & for A st ( On X) c= A holds it c= A;

      existence

      proof

        defpred P[ Ordinal] means ( On X) c= $1;

        x in ( On X) implies x is Ordinal by ORDINAL1:def 9;

        then

        reconsider A = ( union ( On X)) as epsilon-transitive epsilon-connected set by ORDINAL1: 23;

        ( On X) c= ( succ A)

        proof

          let x be object;

          assume

           A1: x in ( On X);

          then

          reconsider B = x as Ordinal by ORDINAL1:def 9;

          B c= A by A1, ZFMISC_1: 74;

          hence thesis by ORDINAL1: 22;

        end;

        then

         A2: ex A st P[A];

        thus ex F be Ordinal st P[F] & for A st P[A] holds F c= A from ORDINAL1:sch 1( A2);

      end;

      uniqueness ;

    end

    theorem :: ORDINAL2:14

    A in X implies ( inf X) c= A

    proof

      assume A in X;

      then A in ( On X) by ORDINAL1:def 9;

      hence thesis by SETFAM_1: 3;

    end;

    theorem :: ORDINAL2:15

    ( On X) <> 0 & (for A st A in X holds D c= A) implies D c= ( inf X)

    proof

      assume that

       A1: ( On X) <> 0 and

       A2: for A st A in X holds D c= A;

      let x be object such that

       A3: x in D;

      for Y st Y in ( On X) holds x in Y

      proof

        let Y;

        assume

         A4: Y in ( On X);

        then

        reconsider A = Y as Ordinal by ORDINAL1:def 9;

        A in X by A4, ORDINAL1:def 9;

        then D c= A by A2;

        hence thesis by A3;

      end;

      hence thesis by A1, SETFAM_1:def 1;

    end;

    theorem :: ORDINAL2:16

    A in X & X c= Y implies ( inf Y) c= ( inf X)

    proof

      assume A in X;

      then

       A1: ( On X) <> 0 by ORDINAL1:def 9;

      assume X c= Y;

      then ( On X) c= ( On Y) by Th9;

      hence thesis by A1, SETFAM_1: 6;

    end;

    theorem :: ORDINAL2:17

    A in X implies ( inf X) in X

    proof

      defpred P[ Ordinal] means $1 in X;

      assume A in X;

      then

       A1: ex A st P[A];

      consider A such that

       A2: P[A] & for B st P[B] holds A c= B from ORDINAL1:sch 1( A1);

      

       A3: A in ( On X) by A2, ORDINAL1:def 9;

       A4:

      now

        let x be object;

        thus x in A implies for Y st Y in ( On X) holds x in Y

        proof

          assume

           A5: x in A;

          let Y;

          assume

           A6: Y in ( On X);

          then

          reconsider B = Y as Ordinal by ORDINAL1:def 9;

          Y in X by A6, ORDINAL1:def 9;

          then A c= B by A2;

          hence thesis by A5;

        end;

        assume for Y st Y in ( On X) holds x in Y;

        hence x in A by A3;

      end;

      ( On X) <> 0 by A2, ORDINAL1:def 9;

      hence thesis by A2, A4, SETFAM_1:def 1;

    end;

    theorem :: ORDINAL2:18

    

     Th18: ( sup A) = A

    proof

      ( On A) = A & for B st ( On A) c= B holds A c= B by Th8;

      hence thesis by Def3;

    end;

    theorem :: ORDINAL2:19

    

     Th19: A in X implies A in ( sup X)

    proof

      assume A in X;

      then

       A1: A in ( On X) by ORDINAL1:def 9;

      ( On X) c= ( sup X) by Def3;

      hence thesis by A1;

    end;

    theorem :: ORDINAL2:20

    

     Th20: (for A st A in X holds A in D) implies ( sup X) c= D

    proof

      assume

       A1: for A st A in X holds A in D;

      ( On X) c= D

      proof

        let x be object;

        assume

         A2: x in ( On X);

        then

        reconsider A = x as Ordinal by ORDINAL1:def 9;

        A in X by A2, ORDINAL1:def 9;

        hence thesis by A1;

      end;

      hence thesis by Def3;

    end;

    theorem :: ORDINAL2:21

    A in ( sup X) implies ex B st B in X & A c= B

    proof

      assume that

       A1: A in ( sup X) and

       A2: for B st B in X holds not A c= B;

      for B st B in X holds B in A by A2, ORDINAL1: 16;

      then ( sup X) c= A by Th20;

      hence contradiction by A1, ORDINAL1: 5;

    end;

    theorem :: ORDINAL2:22

    X c= Y implies ( sup X) c= ( sup Y)

    proof

      assume X c= Y;

      then

       A1: ( On X) c= ( On Y) by Th9;

      ( On Y) c= ( sup Y) by Def3;

      then ( On X) c= ( sup Y) by A1;

      hence thesis by Def3;

    end;

    theorem :: ORDINAL2:23

    ( sup {A}) = ( succ A)

    proof

      

       A1: ( On {A}) c= ( succ A)

      proof

        let x be object;

        assume x in ( On {A});

        then x in {A} by ORDINAL1:def 9;

        then x = A by TARSKI:def 1;

        hence thesis by ORDINAL1: 6;

      end;

      now

        A in {A} by TARSKI:def 1;

        then

         A2: A in ( On {A}) by ORDINAL1:def 9;

        let B;

        assume ( On {A}) c= B;

        hence ( succ A) c= B by A2, ORDINAL1: 21;

      end;

      hence thesis by A1, Def3;

    end;

    theorem :: ORDINAL2:24

    ( inf X) c= ( sup X)

    proof

      let x be object;

      set y = the Element of ( On X);

      assume

       A1: x in ( inf X);

      then

      reconsider y as Ordinal by ORDINAL1:def 9, SETFAM_1: 1;

      ( On X) c= ( sup X) by Def3;

      then y in ( sup X) by A1, SETFAM_1: 1;

      then

       A2: y c= ( sup X) by ORDINAL1:def 2;

      x in y by A1, SETFAM_1: 1, SETFAM_1:def 1;

      hence thesis by A2;

    end;

    scheme :: ORDINAL2:sch2

    TSLambda { A() -> Ordinal , F( Ordinal) -> set } :

ex L st ( dom L) = A() & for A st A in A() holds (L . A) = F(A);

      deffunc G( object) = F(sup);

      consider f such that

       A1: ( dom f) = A() & for x be object st x in A() holds (f . x) = G(x) from FUNCT_1:sch 3;

      reconsider f as Sequence by A1, ORDINAL1:def 7;

      take L = f;

      thus ( dom L) = A() by A1;

      let A;

      assume A in A();

      

      hence (L . A) = F(sup) by A1

      .= F(sup) by ZFMISC_1: 25

      .= F(A) by Th18;

    end;

    definition

      let f;

      :: ORDINAL2:def4

      attr f is Ordinal-yielding means

      : Def4: ex A st ( rng f) c= A;

    end

    registration

      cluster Ordinal-yielding for Sequence;

      existence

      proof

        set A = the Ordinal;

        set L = the Sequence of A;

        take L, A;

        thus thesis by RELAT_1:def 19;

      end;

    end

    definition

      mode Ordinal-Sequence is Ordinal-yielding Sequence;

    end

    registration

      let A;

      cluster -> Ordinal-yielding for Sequence of A;

      coherence by RELAT_1:def 19;

    end

    registration

      let L be Ordinal-Sequence;

      let A;

      cluster (L | A) -> Ordinal-yielding;

      coherence

      proof

        consider B such that

         A1: ( rng L) c= B by Def4;

        (L | A) is Ordinal-yielding

        proof

          take B;

          ( rng (L | A)) c= ( rng L) by RELAT_1: 70;

          hence thesis by A1;

        end;

        hence thesis;

      end;

    end

    reserve fi,psi for Ordinal-Sequence;

    theorem :: ORDINAL2:25

    

     Th25: A in ( dom fi) implies (fi . A) is Ordinal

    proof

      assume A in ( dom fi);

      then

       A1: (fi . A) in ( rng fi) by FUNCT_1:def 3;

      ex B st ( rng fi) c= B by Def4;

      hence thesis by A1;

    end;

    registration

      let f be Ordinal-Sequence, a be object;

      cluster (f . a) -> ordinal;

      coherence

      proof

        a in ( dom f) or not a in ( dom f);

        hence thesis by Th25, FUNCT_1:def 2;

      end;

    end

    scheme :: ORDINAL2:sch3

    OSLambda { A() -> Ordinal , F( Ordinal) -> Ordinal } :

ex fi st ( dom fi) = A() & for A st A in A() holds (fi . A) = F(A);

      consider L such that

       A1: ( dom L) = A() & for A st A in A() holds (L . A) = F(A) from TSLambda;

      L is Ordinal-yielding

      proof

        take ( sup ( rng L));

        let x be object;

        assume

         A2: x in ( rng L);

        then

        consider y be object such that

         A3: y in ( dom L) and

         A4: x = (L . y) by FUNCT_1:def 3;

        reconsider y as Ordinal by A3;

        (L . y) = F(y) by A1, A3;

        then

         A5: x in ( On ( rng L)) by A2, A4, ORDINAL1:def 9;

        ( On ( rng L)) c= ( sup ( rng L)) by Def3;

        hence thesis by A5;

      end;

      then

      reconsider L as Ordinal-Sequence;

      take fi = L;

      thus ( dom fi) = A() by A1;

      let A;

      assume A in A();

      hence thesis by A1;

    end;

    scheme :: ORDINAL2:sch4

    TSUniq1 { A() -> Ordinal , B() -> object , C( Ordinal, set) -> object , D( Ordinal, Sequence) -> object , L1() -> Sequence , L2() -> Sequence } :

L1() = L2()

      provided

       A1: ( dom L1()) = A()

       and

       A2: 0 in A() implies (L1() . 0 ) = B()

       and

       A3: for A st ( succ A) in A() holds (L1() . ( succ A)) = C(A,.)

       and

       A4: for A st A in A() & A <> 0 & A is limit_ordinal holds (L1() . A) = D(A,|)

       and

       A5: ( dom L2()) = A()

       and

       A6: 0 in A() implies (L2() . 0 ) = B()

       and

       A7: for A st ( succ A) in A() holds (L2() . ( succ A)) = C(A,.)

       and

       A8: for A st A in A() & A <> 0 & A is limit_ordinal holds (L2() . A) = D(A,|);

      defpred P[ object] means (L1() . $1) <> (L2() . $1);

      consider X such that

       A9: for Y be object holds Y in X iff Y in A() & P[Y] from XBOOLE_0:sch 1;

      for b be object holds b in X implies b in A() by A9;

      then

       A10: X c= A();

      assume L1() <> L2();

      then ex a be object st a in A() & (L1() . a) <> (L2() . a) by A1, A5, FUNCT_1: 2;

      then X <> 0 by A9;

      then

      consider B such that

       A11: B in X and

       A12: for C st C in X holds B c= C by A10, ORDINAL1: 20;

      

       A13: B in A() by A9, A11;

      then

       A14: B c= A() by ORDINAL1:def 2;

      then

       A15: ( dom (L1() | B)) = B & ( dom (L2() | B)) = B by A1, A5, RELAT_1: 62;

       A16:

      now

        let C;

        assume

         A17: C in B;

        then not C in X by A12, ORDINAL1: 5;

        hence (L1() . C) = (L2() . C) by A9, A14, A17;

      end;

       A18:

      now

        let a be object;

        assume

         A19: a in B;

        ((L1() | B) . a) = (L1() . a) & ((L2() | B) . a) = (L2() . a) by A15, A19, FUNCT_1: 47;

        hence ((L1() | B) . a) = ((L2() | B) . a) by A16, A19;

      end;

       A20:

      now

        given C such that

         A21: B = ( succ C);

        

         A22: (L1() . C) = ((L1() | B) . C) & (L2() . C) = ((L2() | B) . C) by A21, FUNCT_1: 49, ORDINAL1: 6;

        (L1() . B) = C(C,.) & (L2() . B) = C(C,.) by A3, A7, A13, A21;

        hence (L1() . B) = (L2() . B) by A18, A21, A22, ORDINAL1: 6;

      end;

      now

        assume that

         A23: B <> 0 and

         A24: for C holds B <> ( succ C);

        B is limit_ordinal by A24, ORDINAL1: 29;

        then (L1() . B) = D(B,|) & (L2() . B) = D(B,|) by A4, A8, A13, A23;

        hence (L1() . B) = (L2() . B) by A15, A18, FUNCT_1: 2;

      end;

      hence contradiction by A2, A6, A9, A11, A20;

    end;

    scheme :: ORDINAL2:sch5

    TSExist1 { A() -> Ordinal , B() -> object , C( Ordinal, set) -> object , D( Ordinal, Sequence) -> object } :

ex L st ( dom L) = A() & ( 0 in A() implies (L . 0 ) = B()) & (for A st ( succ A) in A() holds (L . ( succ A)) = C(A,.)) & for A st A in A() & A <> 0 & A is limit_ordinal holds (L . A) = D(A,|);

      defpred P[ Ordinal, Sequence] means ( dom $2) = $1 & ( 0 in $1 implies ($2 . 0 ) = B()) & (for A1 st ( succ A1) in $1 holds ($2 . ( succ A1)) = C(A1,.)) & for A1 st A1 in $1 & A1 <> 0 & A1 is limit_ordinal holds ($2 . A1) = D(A1,|);

      defpred R[ Ordinal] means ex L st P[$1, L];

      

       A1: for B st for C st C in B holds R[C] holds R[B]

      proof

        defpred R[ object, object] means $1 is Ordinal & $2 is Sequence & for A, L st A = $1 & L = $2 holds P[A, L];

        let B such that

         A2: for C st C in B holds ex L st P[C, L];

        

         A3: for a,b,c be object st R[a, b] & R[a, c] holds b = c

        proof

          let a,b,c be object;

          assume that

           A4: a is Ordinal and

           A5: b is Sequence and

           A6: for A, L st A = a & L = b holds P[A, L] and a is Ordinal and

           A7: c is Sequence and

           A8: for A, L st A = a & L = c holds P[A, L];

          reconsider a as Ordinal by A4;

          reconsider c as Sequence by A7;

          

           A9: ( dom c) = a by A8;

          

           A10: for A st A in a & A <> 0 & A is limit_ordinal holds (c . A) = D(A,|) by A8;

          

           A11: for A st ( succ A) in a holds (c . ( succ A)) = C(A,.) by A8;

          

           A12: 0 in a implies (c . 0 ) = B() by A8;

          reconsider b as Sequence by A5;

          

           A13: 0 in a implies (b . 0 ) = B() by A6;

          

           A14: for A st ( succ A) in a holds (b . ( succ A)) = C(A,.) by A6;

          

           A15: for A st A in a & A <> 0 & A is limit_ordinal holds (b . A) = D(A,|) by A6;

          

           A16: ( dom b) = a by A6;

          b = c from TSUniq1( A16, A13, A14, A15, A9, A12, A11, A10);

          hence thesis;

        end;

        consider G be Function such that

         A17: for a,b be object holds [a, b] in G iff a in B & R[a, b] from FUNCT_1:sch 1( A3);

        defpred Q[ object, object] means ex A, L st A = $1 & L = (G . $1) & (A = 0 & $2 = B() or (ex B st A = ( succ B) & $2 = C(B,.)) or A <> 0 & A is limit_ordinal & $2 = D(A,L));

        

         A18: ( dom G) = B

        proof

          thus for a be object holds a in ( dom G) implies a in B

          proof

            let a be object;

            assume a in ( dom G);

            then ex b be object st [a, b] in G by XTUPLE_0:def 12;

            hence thesis by A17;

          end;

          let a be object;

          assume

           A19: a in B;

          then

          reconsider a9 = a as Ordinal;

          consider L such that

           A20: P[a9, L] by A2, A19;

          for A holds for K be Sequence holds A = a9 & K = L implies P[A, K] by A20;

          then [a9, L] in G by A17, A19;

          hence thesis by XTUPLE_0:def 12;

        end;

        

         A21: for a be object st a in B holds ex b be object st Q[a, b]

        proof

          let a be object;

          assume

           A22: a in B;

          then

          reconsider A = a as Ordinal;

          consider c be object such that

           A23: [a, c] in G by A18, A22, XTUPLE_0:def 12;

          reconsider L = c as Sequence by A17, A23;

           A24:

          now

            given C such that

             A25: A = ( succ C);

            thus ex b be object st Q[a, b]

            proof

              take C(C,.), A, L;

              thus A = a & L = (G . a) by A23, FUNCT_1: 1;

              thus thesis by A25;

            end;

          end;

           A26:

          now

            assume

             A27: A <> 0 & for C holds A <> ( succ C);

            thus Q[a, D(A,L)]

            proof

              take A, L;

              thus A = a & L = (G . a) by A23, FUNCT_1: 1;

              thus thesis by A27, ORDINAL1: 29;

            end;

          end;

          now

            assume

             A28: A = 0 ;

            thus Q[a, B()]

            proof

              take A, L;

              thus A = a & L = (G . a) by A23, FUNCT_1: 1;

              thus thesis by A28;

            end;

          end;

          hence thesis by A24, A26;

        end;

        

         A29: for a,b,c be object st a in B & Q[a, b] & Q[a, c] holds b = c

        proof

          let a,b,c be object such that a in B;

          given Ab be Ordinal, Lb be Sequence such that

           A30: Ab = a and

           A31: Lb = (G . a) and

           A32: Ab = 0 & b = B() or (ex B st Ab = ( succ B) & b = C(B,.)) or Ab <> 0 & Ab is limit_ordinal & b = D(Ab,Lb);

          given Ac be Ordinal, Lc be Sequence such that

           A33: Ac = a and

           A34: Lc = (G . a) and

           A35: Ac = 0 & c = B() or (ex B st Ac = ( succ B) & c = C(B,.)) or Ac <> 0 & Ac is limit_ordinal & c = D(Ac,Lc);

          now

            given C such that

             A36: Ab = ( succ C);

            consider A such that

             A37: Ab = ( succ A) and

             A38: b = C(A,.) by A32, A36, ORDINAL1: 29;

            consider D such that

             A39: Ac = ( succ D) and

             A40: c = C(D,.) by A30, A33, A35, A36, ORDINAL1: 29;

            A = D by A30, A33, A37, A39, ORDINAL1: 7;

            hence thesis by A31, A34, A38, A40;

          end;

          hence thesis by A30, A31, A32, A33, A34, A35;

        end;

        consider F be Function such that

         A41: ( dom F) = B & for a be object st a in B holds Q[a, (F . a)] from FUNCT_1:sch 2( A29, A21);

        reconsider L = F as Sequence by A41, ORDINAL1:def 7;

        take L;

        thus ( dom L) = B by A41;

        thus 0 in B implies (L . 0 ) = B()

        proof

          assume 0 in B;

          then ex A be Ordinal, K be Sequence st A = 0 & K = (G . 0 ) & (A = 0 & (F . 0 ) = B() or (ex B st A = ( succ B) & (F . 0 ) = C(B,.)) or A <> 0 & A is limit_ordinal & (F . 0 ) = D(A,K)) by A41;

          hence thesis;

        end;

        

         A42: for A, L1 st A in B & L1 = (G . A) holds (L | A) = L1

        proof

          defpred Q[ Ordinal] means for L1 st $1 in B & L1 = (G . $1) holds (L | $1) = L1;

          

           A43: for A st for C st C in A holds Q[C] holds Q[A]

          proof

            let A such that for C st C in A holds for L1 st C in B & L1 = (G . C) holds (L | C) = L1;

            let L1;

            assume that

             A44: A in B and

             A45: L1 = (G . A);

            

             A46: [A, L1] in G by A18, A44, A45, FUNCT_1: 1;

            then

             A47: P[A, L1] by A17;

             A48:

            now

              let x be object;

              assume

               A49: x in A;

              then

              reconsider x9 = x as Ordinal;

              

               A50: x9 in B by A44, A49, ORDINAL1: 10;

              then

              consider A1, L2 such that

               A51: A1 = x9 and

               A52: L2 = (G . x9) and

               A53: A1 = 0 & (L . x9) = B() or (ex B st A1 = ( succ B) & (L . x9) = C(B,.)) or A1 <> 0 & A1 is limit_ordinal & (L . x9) = D(A1,L2) by A41;

              for D, L3 st D = x9 & L3 = (L1 | x9) holds P[D, L3]

              proof

                let D, L3 such that

                 A54: D = x9 and

                 A55: L3 = (L1 | x9);

                x9 c= A by A49, ORDINAL1:def 2;

                hence ( dom L3) = D by A47, A54, A55, RELAT_1: 62;

                thus 0 in D implies (L3 . 0 ) = B() by A47, A49, A54, A55, FUNCT_1: 49, ORDINAL1: 10;

                thus ( succ C) in D implies (L3 . ( succ C)) = C(C,.)

                proof

                  assume

                   A56: ( succ C) in D;

                  C in ( succ C) by ORDINAL1: 6;

                  then

                   A57: ((L1 | x9) . C) = (L1 . C) by A54, A56, FUNCT_1: 49, ORDINAL1: 10;

                  ( succ C) in A & ((L1 | x9) . ( succ C)) = (L1 . ( succ C)) by A49, A54, A56, FUNCT_1: 49, ORDINAL1: 10;

                  hence thesis by A17, A46, A55, A57;

                end;

                let C;

                assume that

                 A58: C in D and

                 A59: C <> 0 & C is limit_ordinal;

                C c= x9 by A54, A58, ORDINAL1:def 2;

                then

                 A60: (L1 | C) = (L3 | C) by A55, FUNCT_1: 51;

                C in A by A49, A54, A58, ORDINAL1: 10;

                then (L1 . C) = D(C,|) by A17, A46, A59, A60;

                hence thesis by A54, A55, A58, FUNCT_1: 49;

              end;

              then [x9, (L1 | x9)] in G by A17, A50;

              then

               A61: (L1 | x9) = L2 by A52, FUNCT_1: 1;

              

               A62: ((L | A) . x) = (L . x) by A49, FUNCT_1: 49;

              now

                given D such that

                 A63: x9 = ( succ D);

                

                 A64: (L1 . x) = C(D,.) by A17, A46, A49, A63;

                consider C such that

                 A65: A1 = ( succ C) and

                 A66: (L . x9) = C(C,.) by A51, A53, A63, ORDINAL1: 29;

                C = D by A51, A63, A65, ORDINAL1: 7;

                hence (L1 . x) = ((L | A) . x) by A62, A61, A63, A66, A64, FUNCT_1: 49, ORDINAL1: 6;

              end;

              hence (L1 . x) = ((L | A) . x) by A17, A46, A49, A51, A53, A62, A61;

            end;

            A c= ( dom L) by A41, A44, ORDINAL1:def 2;

            then ( dom (L | A)) = A by RELAT_1: 62;

            hence thesis by A47, A48, FUNCT_1: 2;

          end;

          thus for A holds Q[A] from ORDINAL1:sch 2( A43);

        end;

        thus ( succ A) in B implies (L . ( succ A)) = C(A,.)

        proof

          assume

           A67: ( succ A) in B;

          then

          consider C be Ordinal, K be Sequence such that

           A68: C = ( succ A) and

           A69: K = (G . ( succ A)) and

           A70: C = 0 & (F . ( succ A)) = B() or (ex B st C = ( succ B) & (F . ( succ A)) = C(B,.)) or C <> 0 & C is limit_ordinal & (F . ( succ A)) = D(C,K) by A41;

          

           A71: K = (L | ( succ A)) by A42, A67, A69;

          consider D such that

           A72: C = ( succ D) and

           A73: (F . ( succ A)) = C(D,.) by A68, A70, ORDINAL1: 29;

          A = D by A68, A72, ORDINAL1: 7;

          hence thesis by A73, A71, FUNCT_1: 49, ORDINAL1: 6;

        end;

        let D;

        assume that

         A74: D in B and

         A75: D <> 0 & D is limit_ordinal;

        ex A be Ordinal, K be Sequence st A = D & K = (G . D) & (A = 0 & (F . D) = B() or (ex B st A = ( succ B) & (F . D) = C(B,.)) or A <> 0 & A is limit_ordinal & (F . D) = D(A,K)) by A41, A74;

        hence thesis by A42, A74, A75, ORDINAL1: 29;

      end;

      for A holds R[A] from ORDINAL1:sch 2( A1);

      hence thesis;

    end;

    scheme :: ORDINAL2:sch6

    TSResult { L() -> Sequence , F( Ordinal) -> set , A() -> Ordinal , B() -> set , C( Ordinal, set) -> set , D( Ordinal, Sequence) -> set } :

for A st A in ( dom L()) holds (L() . A) = F(A)

      provided

       A1: for A, x holds x = F(A) iff ex L st x = ( last L) & ( dom L) = ( succ A) & (L . 0 ) = B() & (for C st ( succ C) in ( succ A) holds (L . ( succ C)) = C(C,.)) & for C st C in ( succ A) & C <> 0 & C is limit_ordinal holds (L . C) = D(C,|)

       and

       A2: ( dom L()) = A()

       and

       A3: 0 in A() implies (L() . 0 ) = B()

       and

       A4: for A st ( succ A) in A() holds (L() . ( succ A)) = C(A,.)

       and

       A5: for A st A in A() & A <> 0 & A is limit_ordinal holds (L() . A) = D(A,|);

      let A;

      set L = (L() | ( succ A));

      assume A in ( dom L());

      then

       A6: ( succ A) c= ( dom L()) by ORDINAL1: 21;

      

       A7: for C st ( succ C) in ( succ A) holds (L . ( succ C)) = C(C,.)

      proof

        let C such that

         A8: ( succ C) in ( succ A);

        C in ( succ C) by ORDINAL1: 6;

        then

         A9: (L . C) = (L() . C) by A8, FUNCT_1: 49, ORDINAL1: 10;

        (L . ( succ C)) = (L() . ( succ C)) by A8, FUNCT_1: 49;

        hence thesis by A2, A4, A6, A8, A9;

      end;

      

       A10: for C st C in ( succ A) & C <> 0 & C is limit_ordinal holds (L . C) = D(C,|)

      proof

        let C;

        assume that

         A11: C in ( succ A) and

         A12: C <> 0 & C is limit_ordinal;

        C c= ( succ A) by A11, ORDINAL1:def 2;

        then

         A13: (L | C) = (L() | C) by FUNCT_1: 51;

        (L . C) = (L() . C) by A11, FUNCT_1: 49;

        hence thesis by A2, A5, A6, A11, A12, A13;

      end;

       0 c= ( succ A);

      then 0 c< ( succ A);

      then

       A14: 0 in ( succ A) & (L . 0 ) = (L() . 0 ) by FUNCT_1: 49, ORDINAL1: 11;

      

       A15: ( dom L) = ( succ A) by A6, RELAT_1: 62;

      then A in ( succ A) & ( last L) = (L . A) by Th2, ORDINAL1: 21;

      then ( last L) = (L() . A) by FUNCT_1: 49;

      hence thesis by A1, A2, A3, A6, A15, A14, A7, A10;

    end;

    scheme :: ORDINAL2:sch7

    TSDef { A() -> Ordinal , B() -> set , C( Ordinal, set) -> set , D( Ordinal, Sequence) -> set } :

(ex x, L st x = ( last L) & ( dom L) = ( succ A()) & (L . 0 ) = B() & (for C st ( succ C) in ( succ A()) holds (L . ( succ C)) = C(C,.)) & for C st C in ( succ A()) & C <> 0 & C is limit_ordinal holds (L . C) = D(C,|)) & for x1,x2 be set st (ex L st x1 = ( last L) & ( dom L) = ( succ A()) & (L . 0 ) = B() & (for C st ( succ C) in ( succ A()) holds (L . ( succ C)) = C(C,.)) & for C st C in ( succ A()) & C <> 0 & C is limit_ordinal holds (L . C) = D(C,|)) & (ex L st x2 = ( last L) & ( dom L) = ( succ A()) & (L . 0 ) = B() & (for C st ( succ C) in ( succ A()) holds (L . ( succ C)) = C(C,.)) & for C st C in ( succ A()) & C <> 0 & C is limit_ordinal holds (L . C) = D(C,|)) holds x1 = x2;

      consider L such that

       A1: ( dom L) = ( succ A()) & ( 0 in ( succ A()) implies (L . 0 ) = B()) & (for C st ( succ C) in ( succ A()) holds (L . ( succ C)) = C(C,.)) & for C st C in ( succ A()) & C <> 0 & C is limit_ordinal holds (L . C) = D(C,|) from TSExist1;

      thus ex x, L st x = ( last L) & ( dom L) = ( succ A()) & (L . 0 ) = B() & (for C st ( succ C) in ( succ A()) holds (L . ( succ C)) = C(C,.)) & for C st C in ( succ A()) & C <> 0 & C is limit_ordinal holds (L . C) = D(C,|)

      proof

        take x = ( last L), L;

        thus x = ( last L) & ( dom L) = ( succ A()) by A1;

         0 c= ( succ A());

        then 0 c< ( succ A());

        hence thesis by A1, ORDINAL1: 11;

      end;

      let x1,x2 be set;

      given L1 such that

       A2: x1 = ( last L1) and

       A3: ( dom L1) = ( succ A()) and

       A4: (L1 . 0 ) = B() and

       A5: for C st ( succ C) in ( succ A()) holds (L1 . ( succ C)) = C(C,.) and

       A6: for C st C in ( succ A()) & C <> 0 & C is limit_ordinal holds (L1 . C) = D(C,|);

      

       A7: 0 in ( succ A()) implies (L1 . 0 ) = B() by A4;

      given L2 such that

       A8: x2 = ( last L2) and

       A9: ( dom L2) = ( succ A()) and

       A10: (L2 . 0 ) = B() and

       A11: for C st ( succ C) in ( succ A()) holds (L2 . ( succ C)) = C(C,.) and

       A12: for C st C in ( succ A()) & C <> 0 & C is limit_ordinal holds (L2 . C) = D(C,|);

      

       A13: 0 in ( succ A()) implies (L2 . 0 ) = B() by A10;

      L1 = L2 from TSUniq1( A3, A7, A5, A6, A9, A13, A11, A12);

      hence thesis by A2, A8;

    end;

    scheme :: ORDINAL2:sch8

    TSResult0 { F( Ordinal) -> set , B() -> set , C( Ordinal, set) -> set , D( Ordinal, Sequence) -> set } :

F(0) = B()

      provided

       A1: for A, x holds x = F(A) iff ex L st x = ( last L) & ( dom L) = ( succ A) & (L . 0 ) = B() & (for C st ( succ C) in ( succ A) holds (L . ( succ C)) = C(C,.)) & for C st C in ( succ A) & C <> 0 & C is limit_ordinal holds (L . C) = D(C,|);

      consider L such that

       A2: ( dom L) = ( succ 0 ) & ( 0 in ( succ 0 ) implies (L . 0 ) = B()) & (for A st ( succ A) in ( succ 0 ) holds (L . ( succ A)) = C(A,.)) & for A st A in ( succ 0 ) & A <> 0 & A is limit_ordinal holds (L . A) = D(A,|) from TSExist1;

      B() = ( last L) by A2, Th2, ORDINAL1: 6;

      hence thesis by A1, A2, ORDINAL1: 6;

    end;

    scheme :: ORDINAL2:sch9

    TSResultS { B() -> set , C( Ordinal, set) -> set , D( Ordinal, Sequence) -> set , F( Ordinal) -> set } :

for A holds F(succ) = C(A,F)

      provided

       A1: for A, x holds x = F(A) iff ex L st x = ( last L) & ( dom L) = ( succ A) & (L . 0 ) = B() & (for C st ( succ C) in ( succ A) holds (L . ( succ C)) = C(C,.)) & for C st C in ( succ A) & C <> 0 & C is limit_ordinal holds (L . C) = D(C,|);

      let A;

      consider L such that

       A2: ( dom L) = ( succ ( succ A)) and

       A3: 0 in ( succ ( succ A)) implies (L . 0 ) = B() and

       A4: for C st ( succ C) in ( succ ( succ A)) holds (L . ( succ C)) = C(C,.) and

       A5: for C st C in ( succ ( succ A)) & C <> 0 & C is limit_ordinal holds (L . C) = D(C,|) from TSExist1;

      

       A6: for A, x holds x = F(A) iff ex L st x = ( last L) & ( dom L) = ( succ A) & (L . 0 ) = B() & (for C st ( succ C) in ( succ A) holds (L . ( succ C)) = C(C,.)) & for C st C in ( succ A) & C <> 0 & C is limit_ordinal holds (L . C) = D(C,|) by A1;

      

       A7: for B st B in ( dom L) holds (L . B) = F(B) from TSResult( A6, A2, A3, A4, A5);

      then

       A8: (L . ( succ A)) = F(succ) by A2, ORDINAL1: 6;

      A in ( succ A) & ( succ A) in ( succ ( succ A)) by ORDINAL1: 6;

      then (L . A) = F(A) by A2, A7, ORDINAL1: 10;

      hence thesis by A4, A8, ORDINAL1: 6;

    end;

    scheme :: ORDINAL2:sch10

    TSResultL { L() -> Sequence , A() -> Ordinal , F( Ordinal) -> set , B() -> set , C( Ordinal, set) -> set , D( Ordinal, Sequence) -> set } :

F(A) = D(A,L)

      provided

       A1: for A, x holds x = F(A) iff ex L st x = ( last L) & ( dom L) = ( succ A) & (L . 0 ) = B() & (for C st ( succ C) in ( succ A) holds (L . ( succ C)) = C(C,.)) & for C st C in ( succ A) & C <> 0 & C is limit_ordinal holds (L . C) = D(C,|)

       and

       A2: A() <> 0 & A() is limit_ordinal

       and

       A3: ( dom L()) = A()

       and

       A4: for A st A in A() holds (L() . A) = F(A);

      

       A5: A() in ( succ A()) by ORDINAL1: 6;

      consider L such that

       A6: ( dom L) = ( succ A()) and

       A7: 0 in ( succ A()) implies (L . 0 ) = B() and

       A8: for C st ( succ C) in ( succ A()) holds (L . ( succ C)) = C(C,.) and

       A9: for C st C in ( succ A()) & C <> 0 & C is limit_ordinal holds (L . C) = D(C,|) from TSExist1;

      set L1 = (L | A());

      

       A10: for A, x holds x = F(A) iff ex L st x = ( last L) & ( dom L) = ( succ A) & (L . 0 ) = B() & (for C st ( succ C) in ( succ A) holds (L . ( succ C)) = C(C,.)) & for C st C in ( succ A) & C <> 0 & C is limit_ordinal holds (L . C) = D(C,|) by A1;

      

       A11: for B st B in ( dom L) holds (L . B) = F(B) from TSResult( A10, A6, A7, A8, A9);

       A12:

      now

        let x be object;

        assume

         A13: x in A();

        then

        reconsider x9 = x as Ordinal;

        

        thus (L1 . x) = (L . x9) by A13, FUNCT_1: 49

        .= F(x9) by A6, A11, A5, A13, ORDINAL1: 10

        .= (L() . x) by A4, A13;

      end;

      A() c= ( dom L) by A6, A5, ORDINAL1:def 2;

      then ( dom L1) = A() by RELAT_1: 62;

      then L1 = L() by A3, A12, FUNCT_1: 2;

      then (L . A()) = D(A,L) by A2, A9, ORDINAL1: 6;

      hence thesis by A6, A11, ORDINAL1: 6;

    end;

    scheme :: ORDINAL2:sch11

    OSExist { A() -> Ordinal , B() -> Ordinal , C( Ordinal, Ordinal) -> Ordinal , D( Ordinal, Sequence) -> Ordinal } :

ex fi st ( dom fi) = A() & ( 0 in A() implies (fi . 0 ) = B()) & (for A st ( succ A) in A() holds (fi . ( succ A)) = C(A,.)) & for A st A in A() & A <> 0 & A is limit_ordinal holds (fi . A) = D(A,|);

      deffunc CC( Ordinal, set) = C($1,sup);

      consider L such that

       A1: ( dom L) = A() and

       A2: 0 in A() implies (L . 0 ) = B() and

       A3: for A st ( succ A) in A() holds (L . ( succ A)) = CC(A,.) and

       A4: for A st A in A() & A <> 0 & A is limit_ordinal holds (L . A) = D(A,|) from TSExist1;

      L is Ordinal-yielding

      proof

        take ( sup ( rng L));

        let x be object;

        assume

         A5: x in ( rng L);

        then

        consider y be object such that

         A6: y in ( dom L) and

         A7: x = (L . y) by FUNCT_1:def 3;

        reconsider y as Ordinal by A6;

         A8:

        now

          assume that

           A9: y <> 0 and

           A10: for B holds y <> ( succ B);

          y is limit_ordinal by A10, ORDINAL1: 29;

          then (L . y) = D(y,|) by A1, A4, A6, A9;

          hence x is Ordinal by A7;

        end;

        

         A11: ( On ( rng L)) c= ( sup ( rng L)) by Def3;

        now

          given B such that

           A12: y = ( succ B);

          (L . y) = C(B,sup) by A1, A3, A6, A12;

          hence x is Ordinal by A7;

        end;

        then x in ( On ( rng L)) by A1, A2, A5, A6, A7, A8, ORDINAL1:def 9;

        hence thesis by A11;

      end;

      then

      reconsider L as Ordinal-Sequence;

      take fi = L;

      thus ( dom fi) = A() & ( 0 in A() implies (fi . 0 ) = B()) by A1, A2;

      thus for A st ( succ A) in A() holds (fi . ( succ A)) = C(A,.)

      proof

        let A;

        reconsider B = (fi . A) as Ordinal;

        ( sup ( union {B})) = ( sup B) by ZFMISC_1: 25

        .= B by Th18;

        hence thesis by A3;

      end;

      thus thesis by A4;

    end;

    scheme :: ORDINAL2:sch12

    OSResult { fi() -> Ordinal-Sequence , F( Ordinal) -> Ordinal , A() -> Ordinal , B() -> Ordinal , C( Ordinal, Ordinal) -> Ordinal , D( Ordinal, Sequence) -> Ordinal } :

for A st A in ( dom fi()) holds (fi() . A) = F(A)

      provided

       A1: for A, B holds B = F(A) iff ex fi st B = ( last fi) & ( dom fi) = ( succ A) & (fi . 0 ) = B() & (for C st ( succ C) in ( succ A) holds (fi . ( succ C)) = C(C,.)) & for C st C in ( succ A) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|)

       and

       A2: ( dom fi()) = A()

       and

       A3: 0 in A() implies (fi() . 0 ) = B()

       and

       A4: for A st ( succ A) in A() holds (fi() . ( succ A)) = C(A,.)

       and

       A5: for A st A in A() & A <> 0 & A is limit_ordinal holds (fi() . A) = D(A,|);

      let A;

      set fi = (fi() | ( succ A));

      assume A in ( dom fi());

      then

       A6: ( succ A) c= ( dom fi()) by ORDINAL1: 21;

      

       A7: for C st ( succ C) in ( succ A) holds (fi . ( succ C)) = C(C,.)

      proof

        let C such that

         A8: ( succ C) in ( succ A);

        C in ( succ C) by ORDINAL1: 6;

        then

         A9: (fi . C) = (fi() . C) by A8, FUNCT_1: 49, ORDINAL1: 10;

        (fi . ( succ C)) = (fi() . ( succ C)) by A8, FUNCT_1: 49;

        hence thesis by A2, A4, A6, A8, A9;

      end;

      

       A10: for C st C in ( succ A) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|)

      proof

        let C;

        assume that

         A11: C in ( succ A) and

         A12: C <> 0 & C is limit_ordinal;

        C c= ( succ A) by A11, ORDINAL1:def 2;

        then

         A13: (fi | C) = (fi() | C) by FUNCT_1: 51;

        (fi . C) = (fi() . C) by A11, FUNCT_1: 49;

        hence thesis by A2, A5, A6, A11, A12, A13;

      end;

       0 c= ( succ A);

      then 0 c< ( succ A);

      then

       A14: 0 in ( succ A) & (fi . 0 ) = (fi() . 0 ) by FUNCT_1: 49, ORDINAL1: 11;

      

       A15: ( dom fi) = ( succ A) by A6, RELAT_1: 62;

      then A in ( succ A) & ( last fi) = (fi . A) by Th2, ORDINAL1: 21;

      then ( last fi) = (fi() . A) by FUNCT_1: 49;

      hence thesis by A1, A2, A3, A6, A15, A14, A7, A10;

    end;

    scheme :: ORDINAL2:sch13

    OSDef { A() -> Ordinal , B() -> Ordinal , C( Ordinal, Ordinal) -> Ordinal , D( Ordinal, Sequence) -> Ordinal } :

(ex A, fi st A = ( last fi) & ( dom fi) = ( succ A()) & (fi . 0 ) = B() & (for C st ( succ C) in ( succ A()) holds (fi . ( succ C)) = C(C,.)) & for C st C in ( succ A()) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|)) & for A1, A2 st (ex fi st A1 = ( last fi) & ( dom fi) = ( succ A()) & (fi . 0 ) = B() & (for C st ( succ C) in ( succ A()) holds (fi . ( succ C)) = C(C,.)) & for C st C in ( succ A()) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|)) & (ex fi st A2 = ( last fi) & ( dom fi) = ( succ A()) & (fi . 0 ) = B() & (for C st ( succ C) in ( succ A()) holds (fi . ( succ C)) = C(C,.)) & for C st C in ( succ A()) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|)) holds A1 = A2;

      consider fi such that

       A1: ( dom fi) = ( succ A()) & ( 0 in ( succ A()) implies (fi . 0 ) = B()) & (for C st ( succ C) in ( succ A()) holds (fi . ( succ C)) = C(C,.)) & for C st C in ( succ A()) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|) from OSExist;

      reconsider A = ( last fi) as Ordinal;

      thus ex A, fi st A = ( last fi) & ( dom fi) = ( succ A()) & (fi . 0 ) = B() & (for C st ( succ C) in ( succ A()) holds (fi . ( succ C)) = C(C,.)) & for C st C in ( succ A()) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|)

      proof

        take A, fi;

        thus A = ( last fi) & ( dom fi) = ( succ A()) by A1;

         0 c= ( succ A());

        then 0 c< ( succ A());

        hence thesis by A1, ORDINAL1: 11;

      end;

      deffunc CD( Ordinal, Ordinal) = C($1,sup);

      let A1,A2 be Ordinal;

      given L1 be Ordinal-Sequence such that

       A2: A1 = ( last L1) and

       A3: ( dom L1) = ( succ A()) and

       A4: (L1 . 0 ) = B() and

       A5: for C st ( succ C) in ( succ A()) holds (L1 . ( succ C)) = C(C,.) and

       A6: for C st C in ( succ A()) & C <> 0 & C is limit_ordinal holds (L1 . C) = D(C,|);

      

       A7: 0 in ( succ A()) implies (L1 . 0 ) = B() by A4;

      

       A8: for C st ( succ C) in ( succ A()) holds (L1 . ( succ C)) = CD(C,.)

      proof

        let C such that

         A9: ( succ C) in ( succ A());

        reconsider x9 = (L1 . C) as Ordinal;

        ( sup ( union {(L1 . C)})) = ( sup x9) by ZFMISC_1: 25

        .= x9 by Th18;

        hence thesis by A5, A9;

      end;

      given L2 be Ordinal-Sequence such that

       A10: A2 = ( last L2) and

       A11: ( dom L2) = ( succ A()) and

       A12: (L2 . 0 ) = B() and

       A13: for C st ( succ C) in ( succ A()) holds (L2 . ( succ C)) = C(C,.) and

       A14: for C st C in ( succ A()) & C <> 0 & C is limit_ordinal holds (L2 . C) = D(C,|);

      

       A15: for C st C in ( succ A()) & C <> 0 & C is limit_ordinal holds (L2 . C) = D(C,|) by A14;

      

       A16: for C st C in ( succ A()) & C <> 0 & C is limit_ordinal holds (L1 . C) = D(C,|) by A6;

      

       A17: for C st ( succ C) in ( succ A()) holds (L2 . ( succ C)) = CD(C,.)

      proof

        let C such that

         A18: ( succ C) in ( succ A());

        reconsider x9 = (L2 . C) as Ordinal;

        ( sup ( union {(L2 . C)})) = ( sup x9) by ZFMISC_1: 25

        .= x9 by Th18;

        hence thesis by A13, A18;

      end;

      

       A19: 0 in ( succ A()) implies (L2 . 0 ) = B() by A12;

      L1 = L2 from TSUniq1( A3, A7, A8, A16, A11, A19, A17, A15);

      hence thesis by A2, A10;

    end;

    scheme :: ORDINAL2:sch14

    OSResult0 { F( Ordinal) -> Ordinal , B() -> Ordinal , C( Ordinal, Ordinal) -> Ordinal , D( Ordinal, Sequence) -> Ordinal } :

F(0) = B()

      provided

       A1: for A, B holds B = F(A) iff ex fi st B = ( last fi) & ( dom fi) = ( succ A) & (fi . 0 ) = B() & (for C st ( succ C) in ( succ A) holds (fi . ( succ C)) = C(C,.)) & for C st C in ( succ A) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|);

      consider fi such that

       A2: ( dom fi) = ( succ 0 ) & ( 0 in ( succ 0 ) implies (fi . 0 ) = B()) & (for A st ( succ A) in ( succ 0 ) holds (fi . ( succ A)) = C(A,.)) & for A st A in ( succ 0 ) & A <> 0 & A is limit_ordinal holds (fi . A) = D(A,|) from OSExist;

      B() = ( last fi) by A2, Th2, ORDINAL1: 6;

      hence thesis by A1, A2, ORDINAL1: 6;

    end;

    scheme :: ORDINAL2:sch15

    OSResultS { B() -> Ordinal , C( Ordinal, Ordinal) -> Ordinal , D( Ordinal, Sequence) -> Ordinal , F( Ordinal) -> Ordinal } :

for A holds F(succ) = C(A,F)

      provided

       A1: for A, B holds B = F(A) iff ex fi st B = ( last fi) & ( dom fi) = ( succ A) & (fi . 0 ) = B() & (for C st ( succ C) in ( succ A) holds (fi . ( succ C)) = C(C,.)) & for C st C in ( succ A) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|);

      let A;

      consider fi such that

       A2: ( dom fi) = ( succ ( succ A)) and

       A3: 0 in ( succ ( succ A)) implies (fi . 0 ) = B() and

       A4: for C st ( succ C) in ( succ ( succ A)) holds (fi . ( succ C)) = C(C,.) and

       A5: for C st C in ( succ ( succ A)) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|) from OSExist;

      

       A6: for A, B holds B = F(A) iff ex fi st B = ( last fi) & ( dom fi) = ( succ A) & (fi . 0 ) = B() & (for C st ( succ C) in ( succ A) holds (fi . ( succ C)) = C(C,.)) & for C st C in ( succ A) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|) by A1;

      

       A7: for B st B in ( dom fi) holds (fi . B) = F(B) from OSResult( A6, A2, A3, A4, A5);

      then

       A8: (fi . ( succ A)) = F(succ) by A2, ORDINAL1: 6;

      A in ( succ A) & ( succ A) in ( succ ( succ A)) by ORDINAL1: 6;

      then (fi . A) = F(A) by A2, A7, ORDINAL1: 10;

      hence thesis by A4, A8, ORDINAL1: 6;

    end;

    scheme :: ORDINAL2:sch16

    OSResultL { fi() -> Ordinal-Sequence , A() -> Ordinal , F( Ordinal) -> Ordinal , B() -> Ordinal , C( Ordinal, Ordinal) -> Ordinal , D( Ordinal, Sequence) -> Ordinal } :

F(A) = D(A,fi)

      provided

       A1: for A, B holds B = F(A) iff ex fi st B = ( last fi) & ( dom fi) = ( succ A) & (fi . 0 ) = B() & (for C st ( succ C) in ( succ A) holds (fi . ( succ C)) = C(C,.)) & for C st C in ( succ A) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|)

       and

       A2: A() <> 0 & A() is limit_ordinal

       and

       A3: ( dom fi()) = A()

       and

       A4: for A st A in A() holds (fi() . A) = F(A);

      

       A5: A() in ( succ A()) by ORDINAL1: 6;

      consider fi such that

       A6: ( dom fi) = ( succ A()) and

       A7: 0 in ( succ A()) implies (fi . 0 ) = B() and

       A8: for C st ( succ C) in ( succ A()) holds (fi . ( succ C)) = C(C,.) and

       A9: for C st C in ( succ A()) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|) from OSExist;

      set psi = (fi | A());

      

       A10: for A, B holds B = F(A) iff ex fi st B = ( last fi) & ( dom fi) = ( succ A) & (fi . 0 ) = B() & (for C st ( succ C) in ( succ A) holds (fi . ( succ C)) = C(C,.)) & for C st C in ( succ A) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|) by A1;

      

       A11: for B st B in ( dom fi) holds (fi . B) = F(B) from OSResult( A10, A6, A7, A8, A9);

       A12:

      now

        let x be object;

        assume

         A13: x in A();

        then

        reconsider x9 = x as Ordinal;

        

        thus (psi . x) = (fi . x9) by A13, FUNCT_1: 49

        .= F(x9) by A6, A11, A5, A13, ORDINAL1: 10

        .= (fi() . x) by A4, A13;

      end;

      A() c= ( dom fi) by A6, A5, ORDINAL1:def 2;

      then ( dom psi) = A() by RELAT_1: 62;

      then psi = fi() by A3, A12, FUNCT_1: 2;

      then (fi . A()) = D(A,fi) by A2, A9, ORDINAL1: 6;

      hence thesis by A6, A11, ORDINAL1: 6;

    end;

    definition

      let L;

      :: ORDINAL2:def5

      func sup L -> Ordinal equals ( sup ( rng L));

      correctness ;

      :: ORDINAL2:def6

      func inf L -> Ordinal equals ( inf ( rng L));

      correctness ;

    end

    theorem :: ORDINAL2:26

    ( sup L) = ( sup ( rng L)) & ( inf L) = ( inf ( rng L));

    definition

      let L;

      :: ORDINAL2:def7

      func lim_sup L -> Ordinal means ex fi st it = ( inf fi) & ( dom fi) = ( dom L) & for A st A in ( dom L) holds (fi . A) = ( sup ( rng (L | (( dom L) \ A))));

      existence

      proof

        deffunc F( Ordinal) = ( sup ( rng (L | (( dom L) \ $1))));

        consider fi such that

         A1: ( dom fi) = ( dom L) & for A st A in ( dom L) holds (fi . A) = F(A) from OSLambda;

        take ( inf fi), fi;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let A1,A2 be Ordinal;

        given fi such that

         A2: A1 = ( inf fi) & ( dom fi) = ( dom L) and

         A3: for A st A in ( dom L) holds (fi . A) = ( sup ( rng (L | (( dom L) \ A))));

        given psi such that

         A4: A2 = ( inf psi) & ( dom psi) = ( dom L) and

         A5: for A st A in ( dom L) holds (psi . A) = ( sup ( rng (L | (( dom L) \ A))));

        now

          let x be object;

          assume

           A6: x in ( dom L);

          then

          reconsider A = x as Ordinal;

          (fi . A) = ( sup ( rng (L | (( dom L) \ A)))) by A3, A6;

          hence (fi . x) = (psi . x) by A5, A6;

        end;

        hence thesis by A2, A4, FUNCT_1: 2;

      end;

      :: ORDINAL2:def8

      func lim_inf L -> Ordinal means ex fi st it = ( sup fi) & ( dom fi) = ( dom L) & for A st A in ( dom L) holds (fi . A) = ( inf ( rng (L | (( dom L) \ A))));

      existence

      proof

        deffunc F( Ordinal) = ( inf ( rng (L | (( dom L) \ $1))));

        consider fi such that

         A7: ( dom fi) = ( dom L) & for A st A in ( dom L) holds (fi . A) = F(A) from OSLambda;

        take ( sup fi), fi;

        thus thesis by A7;

      end;

      uniqueness

      proof

        let A1,A2 be Ordinal;

        given fi such that

         A8: A1 = ( sup fi) & ( dom fi) = ( dom L) and

         A9: for A st A in ( dom L) holds (fi . A) = ( inf ( rng (L | (( dom L) \ A))));

        given psi such that

         A10: A2 = ( sup psi) & ( dom psi) = ( dom L) and

         A11: for A st A in ( dom L) holds (psi . A) = ( inf ( rng (L | (( dom L) \ A))));

        now

          let x be object;

          assume

           A12: x in ( dom L);

          then

          reconsider A = x as Ordinal;

          (fi . A) = ( inf ( rng (L | (( dom L) \ A)))) by A9, A12;

          hence (fi . x) = (psi . x) by A11, A12;

        end;

        hence thesis by A8, A10, FUNCT_1: 2;

      end;

    end

    definition

      let A, fi;

      :: ORDINAL2:def9

      pred A is_limes_of fi means

      : Def9: ex B st B in ( dom fi) & for C st B c= C & C in ( dom fi) holds (fi . C) = 0 if A = 0

      otherwise for B, C st B in A & A in C holds ex D st D in ( dom fi) & for E be Ordinal st D c= E & E in ( dom fi) holds B in (fi . E) & (fi . E) in C;

      consistency ;

    end

    definition

      let fi;

      given A such that

       A1: A is_limes_of fi;

      :: ORDINAL2:def10

      func lim fi -> Ordinal means

      : Def10: it is_limes_of fi;

      existence by A1;

      uniqueness

      proof

        let A1,A2 be Ordinal such that

         A2: (A1 = 0 & ex B st B in ( dom fi) & for C st B c= C & C in ( dom fi) holds (fi . C) = 0 ) or (A1 <> 0 & for B, C st B in A1 & A1 in C holds ex D st D in ( dom fi) & for E be Ordinal st D c= E & E in ( dom fi) holds B in (fi . E) & (fi . E) in C) and

         A3: (A2 = 0 & ex B st B in ( dom fi) & for C st B c= C & C in ( dom fi) holds (fi . C) = 0 ) or (A2 <> 0 & for B, C st B in A2 & A2 in C holds ex D st D in ( dom fi) & for E be Ordinal st D c= E & E in ( dom fi) holds B in (fi . E) & (fi . E) in C);

         A4:

        now

          set x = the Element of A1;

          reconsider x as Ordinal;

          assume A1 in A2;

          then

          consider D such that

           A5: D in ( dom fi) and

           A6: for A st D c= A & A in ( dom fi) holds A1 in (fi . A) & (fi . A) in ( succ A2) by A3, ORDINAL1: 6;

          now

            assume A1 = 0 ;

            then

            consider B such that

             A7: B in ( dom fi) and

             A8: for C st B c= C & C in ( dom fi) holds (fi . C) = 0 by A2;

            B c= D or D c= B;

            then

            consider E be Ordinal such that

             A9: E = D & B c= D or E = B & D c= B;

            (fi . E) = 0 by A5, A7, A8, A9;

            hence contradiction by A5, A6, A7, A9;

          end;

          then

          consider C such that

           A10: C in ( dom fi) and

           A11: for A st C c= A & A in ( dom fi) holds x in (fi . A) & (fi . A) in ( succ A1) by A2, ORDINAL1: 6;

          C c= D or D c= C;

          then

          consider E be Ordinal such that

           A12: E = D & C c= D or E = C & D c= C;

          (fi . E) in ( succ A1) by A5, A10, A11, A12;

          then

           A13: (fi . E) in A1 or (fi . E) = A1 by ORDINAL1: 8;

          A1 in (fi . E) by A5, A6, A10, A12;

          hence contradiction by A13;

        end;

        set x = the Element of A2;

        reconsider x as Ordinal;

        assume A1 <> A2;

        then A1 in A2 or A2 in A1 by ORDINAL1: 14;

        then

        consider D such that

         A14: D in ( dom fi) and

         A15: for A st D c= A & A in ( dom fi) holds A2 in (fi . A) & (fi . A) in ( succ A1) by A2, A4, ORDINAL1: 6;

        now

          assume A2 = 0 ;

          then

          consider B such that

           A16: B in ( dom fi) and

           A17: for C st B c= C & C in ( dom fi) holds (fi . C) = 0 by A3;

          B c= D or D c= B;

          then

          consider E be Ordinal such that

           A18: E = D & B c= D or E = B & D c= B;

          (fi . E) = 0 by A14, A16, A17, A18;

          hence contradiction by A14, A15, A16, A18;

        end;

        then

        consider C such that

         A19: C in ( dom fi) and

         A20: for A st C c= A & A in ( dom fi) holds x in (fi . A) & (fi . A) in ( succ A2) by A3, ORDINAL1: 6;

        C c= D or D c= C;

        then

        consider E be Ordinal such that

         A21: E = D & C c= D or E = C & D c= C;

        (fi . E) in ( succ A2) by A14, A19, A20, A21;

        then

         A22: (fi . E) in A2 or (fi . E) = A2 by ORDINAL1: 8;

        A2 in (fi . E) by A14, A15, A19, A21;

        hence contradiction by A22;

      end;

    end

    definition

      let A, fi;

      :: ORDINAL2:def11

      func lim (A,fi) -> Ordinal equals ( lim (fi | A));

      correctness ;

    end

    definition

      let L be Ordinal-Sequence;

      :: ORDINAL2:def12

      attr L is increasing means for A, B st A in B & B in ( dom L) holds (L . A) in (L . B);

      :: ORDINAL2:def13

      attr L is continuous means for A, B st A in ( dom L) & A <> 0 & A is limit_ordinal & B = (L . A) holds B is_limes_of (L | A);

    end

    definition

      let A,B be Ordinal;

      :: ORDINAL2:def14

      func A +^ B -> Ordinal means

      : Def14: ex fi st it = ( last fi) & ( dom fi) = ( succ B) & (fi . 0 ) = A & (for C st ( succ C) in ( succ B) holds (fi . ( succ C)) = ( succ (fi . C))) & for C st C in ( succ B) & C <> 0 & C is limit_ordinal holds (fi . C) = ( sup (fi | C));

      correctness

      proof

        deffunc D( Ordinal, Sequence) = ( sup $2);

        deffunc C( Ordinal, Ordinal) = ( succ $2);

        (ex F be Ordinal, fi st F = ( last fi) & ( dom fi) = ( succ B) & (fi . 0 ) = A & (for C st ( succ C) in ( succ B) holds (fi . ( succ C)) = C(C,.)) & for C st C in ( succ B) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|)) & for A1, A2 st (ex fi st A1 = ( last fi) & ( dom fi) = ( succ B) & (fi . 0 ) = A & (for C st ( succ C) in ( succ B) holds (fi . ( succ C)) = C(C,.)) & for C st C in ( succ B) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|)) & (ex fi st A2 = ( last fi) & ( dom fi) = ( succ B) & (fi . 0 ) = A & (for C st ( succ C) in ( succ B) holds (fi . ( succ C)) = C(C,.)) & for C st C in ( succ B) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|)) holds A1 = A2 from OSDef;

        hence thesis;

      end;

    end

    definition

      let A, B;

      :: ORDINAL2:def15

      func A *^ B -> Ordinal means

      : Def15: ex fi st it = ( last fi) & ( dom fi) = ( succ A) & (fi . 0 ) = 0 & (for C st ( succ C) in ( succ A) holds (fi . ( succ C)) = ((fi . C) +^ B)) & for C st C in ( succ A) & C <> 0 & C is limit_ordinal holds (fi . C) = ( union ( sup (fi | C)));

      correctness

      proof

        deffunc D( Ordinal, Ordinal-Sequence) = ( union ( sup $2));

        deffunc C( Ordinal, Ordinal) = ($2 +^ B);

        (ex F be Ordinal, fi st F = ( last fi) & ( dom fi) = ( succ A) & (fi . 0 ) = 0 & (for C st ( succ C) in ( succ A) holds (fi . ( succ C)) = C(C,.)) & for C st C in ( succ A) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|)) & for A1, A2 st (ex fi st A1 = ( last fi) & ( dom fi) = ( succ A) & (fi . 0 ) = 0 & (for C st ( succ C) in ( succ A) holds (fi . ( succ C)) = C(C,.)) & for C st C in ( succ A) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|)) & (ex fi st A2 = ( last fi) & ( dom fi) = ( succ A) & (fi . 0 ) = 0 & (for C st ( succ C) in ( succ A) holds (fi . ( succ C)) = C(C,.)) & for C st C in ( succ A) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|)) holds A1 = A2 from OSDef;

        hence thesis;

      end;

    end

    registration

      let O be Ordinal;

      cluster -> ordinal for Element of O;

      coherence ;

    end

    definition

      let A, B;

      :: ORDINAL2:def16

      func exp (A,B) -> Ordinal means

      : Def16: ex fi st it = ( last fi) & ( dom fi) = ( succ B) & (fi . 0 ) = 1 & (for C st ( succ C) in ( succ B) holds (fi . ( succ C)) = (A *^ (fi . C))) & for C st C in ( succ B) & C <> 0 & C is limit_ordinal holds (fi . C) = ( lim (fi | C));

      correctness

      proof

        deffunc D( Ordinal, Ordinal-Sequence) = ( lim $2);

        deffunc C( Ordinal, Ordinal) = (A *^ $2);

        (ex F be Ordinal, fi st F = ( last fi) & ( dom fi) = ( succ B) & (fi . 0 ) = 1 & (for C st ( succ C) in ( succ B) holds (fi . ( succ C)) = C(C,.)) & for C st C in ( succ B) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|)) & for A1, A2 st (ex fi st A1 = ( last fi) & ( dom fi) = ( succ B) & (fi . 0 ) = 1 & (for C st ( succ C) in ( succ B) holds (fi . ( succ C)) = C(C,.)) & for C st C in ( succ B) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|)) & (ex fi st A2 = ( last fi) & ( dom fi) = ( succ B) & (fi . 0 ) = 1 & (for C st ( succ C) in ( succ B) holds (fi . ( succ C)) = C(C,.)) & for C st C in ( succ B) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|)) holds A1 = A2 from OSDef;

        hence thesis;

      end;

    end

    theorem :: ORDINAL2:27

    

     Th27: (A +^ 0 ) = A

    proof

      deffunc C( Ordinal, Ordinal) = ( succ $2);

      deffunc D( Ordinal, Sequence) = ( sup $2);

      deffunc F( Ordinal) = (A +^ $1);

      

       A1: for B, C holds C = F(B) iff ex fi st C = ( last fi) & ( dom fi) = ( succ B) & (fi . 0 ) = A & (for C st ( succ C) in ( succ B) holds (fi . ( succ C)) = C(C,.)) & for C st C in ( succ B) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|) by Def14;

      thus F(0) = A from OSResult0( A1);

    end;

    theorem :: ORDINAL2:28

    

     Th28: (A +^ ( succ B)) = ( succ (A +^ B))

    proof

      deffunc C( Ordinal, Ordinal) = ( succ $2);

      deffunc D( Ordinal, Sequence) = ( sup $2);

      deffunc F( Ordinal) = (A +^ $1);

      

       A1: for B, C holds C = F(B) iff ex fi st C = ( last fi) & ( dom fi) = ( succ B) & (fi . 0 ) = A & (for C st ( succ C) in ( succ B) holds (fi . ( succ C)) = C(C,.)) & for C st C in ( succ B) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|) by Def14;

      for B holds F(succ) = C(B,F) from OSResultS( A1);

      hence thesis;

    end;

    theorem :: ORDINAL2:29

    

     Th29: B <> 0 & B is limit_ordinal implies for fi st ( dom fi) = B & for C st C in B holds (fi . C) = (A +^ C) holds (A +^ B) = ( sup fi)

    proof

      deffunc C( Ordinal, Ordinal) = ( succ $2);

      deffunc D( Ordinal, Ordinal-Sequence) = ( sup $2);

      assume

       A1: B <> 0 & B is limit_ordinal;

      deffunc F( Ordinal) = (A +^ $1);

      let fi such that

       A2: ( dom fi) = B and

       A3: for C st C in B holds (fi . C) = F(C);

      

       A4: for B, C holds C = F(B) iff ex fi st C = ( last fi) & ( dom fi) = ( succ B) & (fi . 0 ) = A & (for C st ( succ C) in ( succ B) holds (fi . ( succ C)) = C(C,.)) & for C st C in ( succ B) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|) by Def14;

      thus F(B) = D(B,fi) from OSResultL( A4, A1, A2, A3);

    end;

    theorem :: ORDINAL2:30

    

     Th30: ( 0 +^ A) = A

    proof

      defpred P[ Ordinal] means ( 0 +^ $1) = $1;

      

       A1: for A holds P[A] implies P[( succ A)] by Th28;

      

       A2: for A st A <> 0 & A is limit_ordinal & for B st B in A holds P[B] holds P[A]

      proof

        deffunc F( Ordinal) = ( 0 +^ $1);

        let A;

        assume that

         A3: A <> 0 & A is limit_ordinal and

         A4: for B st B in A holds ( 0 +^ B) = B;

        consider fi such that

         A5: ( dom fi) = A & for B st B in A holds (fi . B) = F(B) from OSLambda;

        

         A6: ( rng fi) = A

        proof

          thus for x be object holds x in ( rng fi) implies x in A

          proof

            let x be object;

            assume x in ( rng fi);

            then

            consider y be object such that

             A7: y in ( dom fi) and

             A8: x = (fi . y) by FUNCT_1:def 3;

            reconsider y as Ordinal by A7;

            x = ( 0 +^ y) by A5, A7, A8

            .= y by A4, A5, A7;

            hence thesis by A5, A7;

          end;

          let x be object;

          assume

           A9: x in A;

          then

          reconsider B = x as Ordinal;

          ( 0 +^ B) = B & (fi . B) = ( 0 +^ B) by A4, A5, A9;

          hence thesis by A5, A9, FUNCT_1:def 3;

        end;

        ( 0 +^ A) = ( sup fi) by A3, A5, Th29

        .= ( sup ( rng fi));

        hence thesis by A6, Th18;

      end;

      

       A10: P[ 0 ] by Th27;

      for A holds P[A] from OrdinalInd( A10, A1, A2);

      hence thesis;

    end;

    

     Lm1: 1 = ( succ 0 );

    theorem :: ORDINAL2:31

    (A +^ 1) = ( succ A)

    proof

      

      thus (A +^ 1) = ( succ (A +^ 0 )) by Lm1, Th28

      .= ( succ A) by Th27;

    end;

    theorem :: ORDINAL2:32

    

     Th32: A in B implies (C +^ A) in (C +^ B)

    proof

      defpred P[ Ordinal] means A in $1 implies (C +^ A) in (C +^ $1);

      

       A1: for B st for D st D in B holds P[D] holds P[B]

      proof

        let B such that

         A2: for D st D in B holds A in D implies (C +^ A) in (C +^ D) and

         A3: A in B;

         A4:

        now

          given D such that

           A5: B = ( succ D);

           A6:

          now

            assume A in D;

            then

             A7: (C +^ A) in (C +^ D) by A2, A5, ORDINAL1: 6;

            ( succ (C +^ D)) = (C +^ ( succ D)) & (C +^ D) in ( succ (C +^ D)) by Th28, ORDINAL1: 6;

            hence thesis by A5, A7, ORDINAL1: 10;

          end;

          now

            assume

             A8: not A in D;

            A c< D iff A c= D & A <> D;

            then (C +^ A) in ( succ (C +^ D)) by A3, A5, A8, ORDINAL1: 11, ORDINAL1: 22;

            hence thesis by A5, Th28;

          end;

          hence thesis by A6;

        end;

        now

          deffunc F( Ordinal) = (C +^ $1);

          consider fi such that

           A9: ( dom fi) = B & for D st D in B holds (fi . D) = F(D) from OSLambda;

          (fi . A) = (C +^ A) by A3, A9;

          then

           A10: (C +^ A) in ( rng fi) by A3, A9, FUNCT_1:def 3;

          assume for D holds B <> ( succ D);

          then B is limit_ordinal by ORDINAL1: 29;

          

          then (C +^ B) = ( sup fi) by A3, A9, Th29

          .= ( sup ( rng fi));

          hence thesis by A10, Th19;

        end;

        hence thesis by A4;

      end;

      for B holds P[B] from ORDINAL1:sch 2( A1);

      hence thesis;

    end;

    theorem :: ORDINAL2:33

    

     Th33: A c= B implies (C +^ A) c= (C +^ B)

    proof

      assume

       A1: A c= B;

      now

        assume A <> B;

        then A c< B by A1;

        then (C +^ A) in (C +^ B) by Th32, ORDINAL1: 11;

        hence thesis by ORDINAL1:def 2;

      end;

      hence thesis;

    end;

    theorem :: ORDINAL2:34

    

     Th34: A c= B implies (A +^ C) c= (B +^ C)

    proof

      defpred P[ Ordinal] means (A +^ $1) c= (B +^ $1);

      assume

       A1: A c= B;

      

       A2: for C st for D st D in C holds P[D] holds P[C]

      proof

        let C such that

         A3: for D st D in C holds (A +^ D) c= (B +^ D);

         A4:

        now

          given D such that

           A5: C = ( succ D);

          

           A6: (B +^ C) = ( succ (B +^ D)) by A5, Th28;

          (A +^ D) c= (B +^ D) & (A +^ C) = ( succ (A +^ D)) by A3, A5, Th28, ORDINAL1: 6;

          hence thesis by A6, Th1;

        end;

         A7:

        now

          deffunc F( Ordinal) = (A +^ $1);

          assume that

           A8: C <> 0 and

           A9: for D holds C <> ( succ D);

          consider fi such that

           A10: ( dom fi) = C & for D st D in C holds (fi . D) = F(D) from OSLambda;

           A11:

          now

            let D;

            assume D in ( rng fi);

            then

            consider x be object such that

             A12: x in ( dom fi) and

             A13: D = (fi . x) by FUNCT_1:def 3;

            reconsider x as Ordinal by A12;

            

             A14: (B +^ x) in (B +^ C) by A10, A12, Th32;

            D = (A +^ x) & (A +^ x) c= (B +^ x) by A3, A10, A12, A13;

            hence D in (B +^ C) by A14, ORDINAL1: 12;

          end;

          C is limit_ordinal by A9, ORDINAL1: 29;

          

          then (A +^ C) = ( sup fi) by A8, A10, Th29

          .= ( sup ( rng fi));

          hence thesis by A11, Th20;

        end;

        now

          assume

           A15: C = 0 ;

          then (A +^ C) = A by Th27;

          hence thesis by A1, A15, Th27;

        end;

        hence thesis by A4, A7;

      end;

      for C holds P[C] from ORDINAL1:sch 2( A2);

      hence thesis;

    end;

    theorem :: ORDINAL2:35

    

     Th35: ( 0 *^ A) = 0

    proof

      deffunc D( Ordinal, Sequence) = ( union ( sup $2));

      deffunc F( Ordinal) = ($1 *^ A);

      deffunc C( Ordinal, Ordinal) = ($2 +^ A);

      

       A1: for B, C holds C = F(B) iff ex fi st C = ( last fi) & ( dom fi) = ( succ B) & (fi . 0 ) = 0 & (for C st ( succ C) in ( succ B) holds (fi . ( succ C)) = C(C,.)) & for C st C in ( succ B) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|) by Def15;

      thus F(0) = 0 from OSResult0( A1);

    end;

    theorem :: ORDINAL2:36

    

     Th36: (( succ B) *^ A) = ((B *^ A) +^ A)

    proof

      deffunc D( Ordinal, Sequence) = ( union ( sup $2));

      deffunc F( Ordinal) = ($1 *^ A);

      deffunc C( Ordinal, Ordinal) = ($2 +^ A);

      

       A1: for B, C holds C = F(B) iff ex fi st C = ( last fi) & ( dom fi) = ( succ B) & (fi . 0 ) = 0 & (for C st ( succ C) in ( succ B) holds (fi . ( succ C)) = C(C,.)) & for C st C in ( succ B) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|) by Def15;

      for B holds F(succ) = C(B,F) from OSResultS( A1);

      hence thesis;

    end;

    theorem :: ORDINAL2:37

    

     Th37: B <> 0 & B is limit_ordinal implies for fi st ( dom fi) = B & for C st C in B holds (fi . C) = (C *^ A) holds (B *^ A) = ( union ( sup fi))

    proof

      deffunc D( Ordinal, Ordinal-Sequence) = ( union ( sup $2));

      assume

       A1: B <> 0 & B is limit_ordinal;

      deffunc C( Ordinal, Ordinal) = ($2 +^ A);

      deffunc F( Ordinal) = ($1 *^ A);

      let fi such that

       A2: ( dom fi) = B and

       A3: for C st C in B holds (fi . C) = F(C);

      

       A4: for B, C holds C = F(B) iff ex fi st C = ( last fi) & ( dom fi) = ( succ B) & (fi . 0 ) = 0 & (for C st ( succ C) in ( succ B) holds (fi . ( succ C)) = C(C,.)) & for C st C in ( succ B) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|) by Def15;

      thus F(B) = D(B,fi) from OSResultL( A4, A1, A2, A3);

    end;

    theorem :: ORDINAL2:38

    

     Th38: (A *^ 0 ) = 0

    proof

      defpred P[ Ordinal] means ($1 *^ 0 ) = 0 ;

      

       A1: for A st P[A] holds P[( succ A)]

      proof

        let A;

        assume (A *^ 0 ) = 0 ;

        

        hence (( succ A) *^ 0 ) = ( 0 +^ 0 ) by Th36

        .= 0 by Th27;

      end;

      

       A2: for A st A <> 0 & A is limit_ordinal & for B st B in A holds P[B] holds P[A]

      proof

        deffunc F( Ordinal) = ($1 *^ 0 );

        let A;

        assume that

         A3: A <> 0 and

         A4: A is limit_ordinal and

         A5: for B st B in A holds (B *^ 0 ) = 0 ;

        consider fi such that

         A6: ( dom fi) = A & for B st B in A holds (fi . B) = F(B) from OSLambda;

        ( rng fi) = ( succ 0 )

        proof

          thus for x be object holds x in ( rng fi) implies x in ( succ 0 )

          proof

            let x be object;

            assume x in ( rng fi);

            then

            consider y be object such that

             A7: y in ( dom fi) and

             A8: x = (fi . y) by FUNCT_1:def 3;

            reconsider y as Ordinal by A7;

            x = (y *^ 0 ) by A6, A7, A8

            .= 0 by A5, A6, A7;

            hence thesis by TARSKI:def 1;

          end;

          let x be object;

          assume x in ( succ 0 );

          then

           A9: x = 0 by TARSKI:def 1;

           0 c= A;

          then

           A10: 0 c< A by A3;

          then

           A11: 0 in A by ORDINAL1: 11;

          ( 0 *^ 0 ) = 0 by Th35;

          then (fi . x) = x by A6, A10, A9, ORDINAL1: 11;

          hence thesis by A6, A11, A9, FUNCT_1:def 3;

        end;

        then

         A12: ( sup ( rng fi)) = ( succ 0 ) by Th18;

        (A *^ 0 ) = ( union ( sup fi)) by A3, A4, A6, Th37

        .= ( union ( sup ( rng fi)));

        hence thesis by A12, Th2;

      end;

      

       A13: P[ 0 ] by Th35;

      for A holds P[A] from OrdinalInd( A13, A1, A2);

      hence thesis;

    end;

    theorem :: ORDINAL2:39

    

     Th39: (1 *^ A) = A & (A *^ 1) = A

    proof

      defpred P[ Ordinal] means ($1 *^ ( succ 0 )) = $1;

      

      thus (1 *^ A) = (( 0 *^ A) +^ A) by Lm1, Th36

      .= ( 0 +^ A) by Th35

      .= A by Th30;

      

       A1: for A st for B st B in A holds P[B] holds P[A]

      proof

        let A such that

         A2: for B st B in A holds (B *^ ( succ 0 )) = B;

         A3:

        now

          deffunc F( Ordinal) = ($1 *^ ( succ 0 ));

          assume that

           A4: A <> 0 and

           A5: for B holds A <> ( succ B);

          consider fi such that

           A6: ( dom fi) = A & for D st D in A holds (fi . D) = F(D) from OSLambda;

          

           A7: A = ( rng fi)

          proof

            thus A c= ( rng fi)

            proof

              let x be object;

              assume

               A8: x in A;

              then

              reconsider B = x as Ordinal;

              x = (B *^ ( succ 0 )) by A2, A8

              .= (fi . x) by A6, A8;

              hence thesis by A6, A8, FUNCT_1:def 3;

            end;

            let x be object;

            assume x in ( rng fi);

            then

            consider y be object such that

             A9: y in ( dom fi) and

             A10: x = (fi . y) by FUNCT_1:def 3;

            reconsider y as Ordinal by A9;

            (fi . y) = (y *^ ( succ 0 )) by A6, A9

            .= y by A2, A6, A9;

            hence thesis by A6, A9, A10;

          end;

          

           A11: A is limit_ordinal by A5, ORDINAL1: 29;

          

          then (A *^ ( succ 0 )) = ( union ( sup fi)) by A4, A6, Th37

          .= ( union ( sup ( rng fi)));

          

          hence (A *^ ( succ 0 )) = ( union A) by A7, Th18

          .= A by A11;

        end;

        now

          given B such that

           A12: A = ( succ B);

          

          thus (A *^ ( succ 0 )) = ((B *^ ( succ 0 )) +^ ( succ 0 )) by A12, Th36

          .= (B +^ ( succ 0 )) by A2, A12, ORDINAL1: 6

          .= ( succ (B +^ 0 )) by Th28

          .= A by A12, Th27;

        end;

        hence thesis by A3, Th35;

      end;

      for A holds P[A] from ORDINAL1:sch 2( A1);

      hence thesis;

    end;

    theorem :: ORDINAL2:40

    

     Th40: C <> 0 & A in B implies (A *^ C) in (B *^ C)

    proof

      

       A1: 0 c= C;

      defpred P[ Ordinal] means A in $1 implies (A *^ C) in ($1 *^ C);

      assume C <> 0 ;

      then

       A2: 0 c< C by A1;

      then

       A3: 0 in C by ORDINAL1: 11;

      

       A4: for B st for D st D in B holds P[D] holds P[B]

      proof

        let B such that

         A5: for D st D in B holds A in D implies (A *^ C) in (D *^ C) and

         A6: A in B;

         A7:

        now

          given D such that

           A8: B = ( succ D);

           A9:

          now

            assume A in D;

            then

             A10: (A *^ C) in (D *^ C) by A5, A8, ORDINAL1: 6;

            

             A11: ((D *^ C) +^ 0 ) in ((D *^ C) +^ C) by A2, Th32, ORDINAL1: 11;

            ((D *^ C) +^ C) = (( succ D) *^ C) & ((D *^ C) +^ 0 ) = (D *^ C) by Th27, Th36;

            hence thesis by A8, A10, A11, ORDINAL1: 10;

          end;

          now

            

             A12: ((A *^ C) +^ 0 ) = (A *^ C) by Th27;

            assume

             A13: not A in D;

            A c< D iff A c= D & A <> D;

            then ((A *^ C) +^ 0 ) in ((D *^ C) +^ C) by A3, A6, A8, A13, Th32, ORDINAL1: 11, ORDINAL1: 22;

            hence thesis by A8, A12, Th36;

          end;

          hence thesis by A9;

        end;

        now

          

           A14: ((A *^ C) +^ 0 ) = (A *^ C) & ((A *^ C) +^ 0 ) in ((A *^ C) +^ C) by A2, Th27, Th32, ORDINAL1: 11;

          

           A15: (( succ A) *^ C) = ((A *^ C) +^ C) by Th36;

          deffunc F( Ordinal) = ($1 *^ C);

          consider fi such that

           A16: ( dom fi) = B & for D st D in B holds (fi . D) = F(D) from OSLambda;

          assume for D holds B <> ( succ D);

          then

           A17: B is limit_ordinal by ORDINAL1: 29;

          then

           A18: ( succ A) in B by A6, ORDINAL1: 28;

          then (fi . ( succ A)) = (( succ A) *^ C) by A16;

          then (( succ A) *^ C) in ( rng fi) by A16, A18, FUNCT_1:def 3;

          then

           A19: (( succ A) *^ C) c= ( union ( sup ( rng fi))) by Th19, ZFMISC_1: 74;

          (B *^ C) = ( union ( sup fi)) by A6, A17, A16, Th37

          .= ( union ( sup ( rng fi)));

          hence thesis by A19, A14, A15;

        end;

        hence thesis by A7;

      end;

      for B holds P[B] from ORDINAL1:sch 2( A4);

      hence thesis;

    end;

    theorem :: ORDINAL2:41

    A c= B implies (A *^ C) c= (B *^ C)

    proof

      assume

       A1: A c= B;

       A2:

      now

        assume

         A3: C <> 0 ;

        now

          assume A <> B;

          then A c< B by A1;

          then (A *^ C) in (B *^ C) by A3, Th40, ORDINAL1: 11;

          hence thesis by ORDINAL1:def 2;

        end;

        hence thesis;

      end;

      C = 0 implies thesis by Th38;

      hence thesis by A2;

    end;

    theorem :: ORDINAL2:42

    A c= B implies (C *^ A) c= (C *^ B)

    proof

      assume

       A1: A c= B;

      now

        defpred P[ Ordinal] means ($1 *^ A) c= ($1 *^ B);

        assume

         A2: B <> 0 ;

        

         A3: for C st for D st D in C holds P[D] holds P[C]

        proof

          let C such that

           A4: for D st D in C holds (D *^ A) c= (D *^ B);

           A5:

          now

            given D such that

             A6: C = ( succ D);

            (D *^ A) c= (D *^ B) by A4, A6, ORDINAL1: 6;

            then

             A7: ((D *^ A) +^ A) c= ((D *^ B) +^ A) by Th34;

            

             A8: (C *^ A) = ((D *^ A) +^ A) & (C *^ B) = ((D *^ B) +^ B) by A6, Th36;

            ((D *^ B) +^ A) c= ((D *^ B) +^ B) by A1, Th33;

            hence thesis by A7, A8, XBOOLE_1: 1;

          end;

           A9:

          now

            deffunc F( Ordinal) = ($1 *^ A);

            assume that

             A10: C <> 0 and

             A11: for D holds C <> ( succ D);

            consider fi such that

             A12: ( dom fi) = C & for D st D in C holds (fi . D) = F(D) from OSLambda;

            now

              let D;

              assume D in ( rng fi);

              then

              consider x be object such that

               A13: x in ( dom fi) and

               A14: D = (fi . x) by FUNCT_1:def 3;

              reconsider x as Ordinal by A13;

              

               A15: (x *^ B) in (C *^ B) by A2, A12, A13, Th40;

              D = (x *^ A) & (x *^ A) c= (x *^ B) by A4, A12, A13, A14;

              hence D in (C *^ B) by A15, ORDINAL1: 12;

            end;

            then

             A16: ( sup ( rng fi)) c= (C *^ B) by Th20;

            C is limit_ordinal by A11, ORDINAL1: 29;

            

            then

             A17: (C *^ A) = ( union ( sup fi)) by A10, A12, Th37

            .= ( union ( sup ( rng fi)));

            ( union ( sup ( rng fi))) c= ( sup ( rng fi)) by Th5;

            hence thesis by A17, A16, XBOOLE_1: 1;

          end;

          now

            assume C = 0 ;

            then (C *^ A) = 0 by Th35;

            hence thesis;

          end;

          hence thesis by A5, A9;

        end;

        for C holds P[C] from ORDINAL1:sch 2( A3);

        hence thesis;

      end;

      hence thesis by A1;

    end;

    theorem :: ORDINAL2:43

    

     Th43: ( exp (A, 0 )) = 1

    proof

      deffunc D( Ordinal, Ordinal-Sequence) = ( lim $2);

      deffunc F( Ordinal) = ( exp (A,$1));

      deffunc C( Ordinal, Ordinal) = (A *^ $2);

      

       A1: for B, C holds C = F(B) iff ex fi st C = ( last fi) & ( dom fi) = ( succ B) & (fi . 0 ) = 1 & (for C st ( succ C) in ( succ B) holds (fi . ( succ C)) = C(C,.)) & for C st C in ( succ B) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|) by Def16;

      thus F(0) = 1 from OSResult0( A1);

    end;

    theorem :: ORDINAL2:44

    

     Th44: ( exp (A,( succ B))) = (A *^ ( exp (A,B)))

    proof

      deffunc D( Ordinal, Ordinal-Sequence) = ( lim $2);

      deffunc F( Ordinal) = ( exp (A,$1));

      deffunc C( Ordinal, Ordinal) = (A *^ $2);

      

       A1: for B, C holds C = F(B) iff ex fi st C = ( last fi) & ( dom fi) = ( succ B) & (fi . 0 ) = 1 & (for C st ( succ C) in ( succ B) holds (fi . ( succ C)) = C(C,.)) & for C st C in ( succ B) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|) by Def16;

      for B holds F(succ) = C(B,F) from OSResultS( A1);

      hence thesis;

    end;

    theorem :: ORDINAL2:45

    

     Th45: B <> 0 & B is limit_ordinal implies for fi st ( dom fi) = B & for C st C in B holds (fi . C) = ( exp (A,C)) holds ( exp (A,B)) = ( lim fi)

    proof

      deffunc D( Ordinal, Ordinal-Sequence) = ( lim $2);

      assume

       A1: B <> 0 & B is limit_ordinal;

      deffunc C( Ordinal, Ordinal) = (A *^ $2);

      deffunc F( Ordinal) = ( exp (A,$1));

      let fi such that

       A2: ( dom fi) = B and

       A3: for C st C in B holds (fi . C) = F(C);

      

       A4: for B, C holds C = F(B) iff ex fi st C = ( last fi) & ( dom fi) = ( succ B) & (fi . 0 ) = 1 & (for C st ( succ C) in ( succ B) holds (fi . ( succ C)) = C(C,.)) & for C st C in ( succ B) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|) by Def16;

      thus F(B) = D(B,fi) from OSResultL( A4, A1, A2, A3);

    end;

    theorem :: ORDINAL2:46

    ( exp (A,1)) = A & ( exp (1,A)) = 1

    proof

      defpred P[ Ordinal] means ( exp (1,$1)) = 1;

      

       A1: for A st P[A] holds P[( succ A)]

      proof

        let A;

        assume ( exp (1,A)) = 1;

        

        hence ( exp (1,( succ A))) = (1 *^ 1) by Th44

        .= 1 by Th39;

      end;

      

      thus ( exp (A,1)) = (A *^ ( exp (A, 0 ))) by Lm1, Th44

      .= (A *^ 1) by Th43

      .= A by Th39;

      

       A2: for A st A <> 0 & A is limit_ordinal & for B st B in A holds P[B] holds P[A]

      proof

        deffunc F( Ordinal) = ( exp (1,$1));

        let A such that

         A3: A <> 0 and

         A4: A is limit_ordinal and

         A5: for B st B in A holds ( exp (1,B)) = 1;

        consider fi such that

         A6: ( dom fi) = A & for B st B in A holds (fi . B) = F(B) from OSLambda;

        

         A7: ( rng fi) c= {1}

        proof

          let x be object;

          assume x in ( rng fi);

          then

          consider y be object such that

           A8: y in ( dom fi) and

           A9: x = (fi . y) by FUNCT_1:def 3;

          reconsider y as Ordinal by A8;

          x = ( exp (1,y)) by A6, A8, A9

          .= 1 by A5, A6, A8;

          hence thesis by TARSKI:def 1;

        end;

        now

          set x = the Element of A;

          thus 0 <> 1;

          let B, C such that

           A10: B in 1 & 1 in C;

          reconsider x as Ordinal;

          take D = x;

          thus D in ( dom fi) by A3, A6;

          let E be Ordinal;

          assume that D c= E and

           A11: E in ( dom fi);

          (fi . E) in ( rng fi) by A11, FUNCT_1:def 3;

          hence B in (fi . E) & (fi . E) in C by A7, A10, TARSKI:def 1;

        end;

        then

         A12: 1 is_limes_of fi by Def9;

        ( exp (1,A)) = ( lim fi) by A3, A4, A6, Th45;

        hence thesis by A12, Def10;

      end;

      

       A13: P[ 0 ] by Th43;

      for A holds P[A] from OrdinalInd( A13, A1, A2);

      hence thesis;

    end;

    theorem :: ORDINAL2:47

    for A holds ex B, C st B is limit_ordinal & C is natural & A = (B +^ C)

    proof

      defpred Th[ Ordinal] means ex A1, A2 st A1 is limit_ordinal & A2 is natural & $1 = (A1 +^ A2);

      

       A1: for A st for B st B in A holds Th[B] holds Th[A]

      proof

        let A such that

         A2: for B st B in A holds Th[B];

        

         A3: (ex B st A = ( succ B)) implies Th[A]

        proof

          given B such that

           A4: A = ( succ B);

          consider C, D such that

           A5: C is limit_ordinal and

           A6: D is natural and

           A7: B = (C +^ D) by A2, A4, ORDINAL1: 6;

          take C, E = ( succ D);

          thus C is limit_ordinal by A5;

          thus E in omega by A6, ORDINAL1:def 12;

          thus thesis by A4, A7, Th28;

        end;

        (for B holds A <> ( succ B)) implies Th[A]

        proof

          assume

           A8: for D holds A <> ( succ D);

          take B = A, C = 0 ;

          thus B is limit_ordinal by A8, ORDINAL1: 29;

          thus C in omega by ORDINAL1:def 11;

          thus thesis by Th27;

        end;

        hence thesis by A3;

      end;

      thus for A holds Th[A] from ORDINAL1:sch 2( A1);

    end;

    registration

      let X be set, o be Ordinal;

      cluster (X --> o) -> Ordinal-yielding;

      coherence

      proof

        ( rng (X --> o)) c= {o} & {o} c= ( succ o) by FUNCOP_1: 13, XBOOLE_1: 7;

        then ( rng (X --> o)) c= ( succ o);

        hence thesis;

      end;

    end

    registration

      let O be Ordinal, x be object;

      cluster (O --> x) -> Sequence-like;

      coherence ;

    end

    definition

      let A,B be Ordinal;

      :: ORDINAL2:def17

      pred A is_cofinal_with B means ex xi be Ordinal-Sequence st ( dom xi) = B & ( rng xi) c= A & xi is increasing & A = ( sup xi);

      reflexivity

      proof

        let A;

        

         A1: ( dom ( id A)) = A by RELAT_1: 45;

        then

        reconsider xi = ( id A) as Sequence by ORDINAL1:def 7;

        

         A2: ( rng ( id A)) = A by RELAT_1: 45;

        then

        reconsider xi as Ordinal-Sequence by Def4;

        take xi;

        thus ( dom xi) = A & ( rng xi) c= A by RELAT_1: 45;

        thus xi is increasing

        proof

          let B, C;

          assume that

           A3: B in C and

           A4: C in ( dom xi);

          (xi . C) = C by A1, A4, FUNCT_1: 18;

          hence thesis by A1, A3, A4, FUNCT_1: 18, ORDINAL1: 10;

        end;

        thus thesis by A2, Th18;

      end;

    end

    reserve e,u for set;

    theorem :: ORDINAL2:48

    

     Th48: e in ( rng psi) implies e is Ordinal

    proof

      assume e in ( rng psi);

      then ex u be object st u in ( dom psi) & e = (psi . u) by FUNCT_1:def 3;

      hence thesis;

    end;

    theorem :: ORDINAL2:49

    ( rng psi) c= ( sup psi)

    proof

      let e be object;

      assume

       A1: e in ( rng psi);

      then e is Ordinal by Th48;

      hence thesis by A1, Th19;

    end;

    theorem :: ORDINAL2:50

    A is_cofinal_with 0 implies A = 0

    proof

      given psi such that

       A1: ( dom psi) = 0 and ( rng psi) c= A and psi is increasing and

       A2: A = ( sup psi);

      

      thus A = ( sup 0 ) by A1, A2, RELAT_1: 42

      .= 0 by Th18;

    end;

    scheme :: ORDINAL2:sch17

    OmegaInd { a() -> Nat , P[ object] } :

P[a()]

      provided

       A1: P[ 0 ]

       and

       A2: for a be Nat st P[a] holds P[( succ a)];

      defpred P[ Ordinal] means $1 is natural implies P[$1];

       A3:

      now

        let A;

        assume

         A4: P[A];

        now

          assume ( succ A) is natural;

          then

           A5: ( succ A) in omega ;

          A in ( succ A) by ORDINAL1: 6;

          then A is Element of omega by A5, ORDINAL1: 10;

          hence P[( succ A)] by A2, A4;

        end;

        hence P[( succ A)];

      end;

       A6:

      now

        let A;

        assume

         A7: A <> 0 ;

         0 c= A;

        then 0 c< A by A7;

        then

         A8: 0 in A by ORDINAL1: 11;

        

         A9: not A in A;

        assume A is limit_ordinal;

        then omega c= A by A8, ORDINAL1:def 11;

        then not A in omega by A9;

        hence (for B st B in A holds P[B]) implies P[A] by ORDINAL1:def 12;

      end;

      

       A10: P[ 0 ] by A1;

      for A holds P[A] from OrdinalInd( A10, A3, A6);

      hence thesis;

    end;

    registration

      let a,b be Nat;

      cluster (a +^ b) -> natural;

      coherence

      proof

        defpred P[ Nat] means (a +^ $1) is natural;

         A1:

        now

          let b be Nat;

          assume P[b];

          then

          reconsider c = (a +^ b) as Nat;

          (a +^ ( succ b)) = ( succ c) by Th28;

          hence P[( succ b)];

        end;

        

         A2: P[ 0 ] by Th27;

        thus P[b] from OmegaInd( A2, A1);

      end;

    end

    registration

      let x,y be set, a,b be Nat;

      cluster ( IFEQ (x,y,a,b)) -> natural;

      coherence

      proof

        per cases ;

          suppose x = y;

          hence thesis by FUNCOP_1:def 8;

        end;

          suppose x <> y;

          hence thesis by FUNCOP_1:def 8;

        end;

      end;

    end

    scheme :: ORDINAL2:sch18

    LambdaRecEx { A() -> set , G( set, set) -> set } :

ex f be Function st ( dom f) = omega & (f . 0 ) = A() & for n be Nat holds (f . ( succ n)) = G(n,.);

      deffunc D( set, set) = 0 ;

      consider L be Sequence such that

       A1: ( dom L) = omega and

       A2: 0 in omega implies (L . 0 ) = A() and

       A3: for A be Ordinal st ( succ A) in omega holds (L . ( succ A)) = G(A,.) and for A be Ordinal st A in omega & A <> 0 & A is limit_ordinal holds (L . A) = D(A,|) from TSExist1;

      take L;

      thus ( dom L) = omega by A1;

       0 in omega by ORDINAL1:def 12;

      hence (L . 0 ) = A() by A2;

      let n be Nat;

      ( succ n) in omega by ORDINAL1:def 12;

      hence thesis by A3;

    end;

    reserve n for Nat;

    scheme :: ORDINAL2:sch19

    RecUn { A() -> set , F,G() -> Function , P[ set, set, set] } :

F() = G()

      provided

       A1: ( dom F()) = omega

       and

       A2: (F() . 0 ) = A()

       and

       A3: for n holds P[n, (F() . n), (F() . ( succ n))]

       and

       A4: ( dom G()) = omega

       and

       A5: (G() . 0 ) = A()

       and

       A6: for n holds P[n, (G() . n), (G() . ( succ n))]

       and

       A7: for n holds for x,y1,y2 be set st P[n, x, y1] & P[n, x, y2] holds y1 = y2;

      defpred P[ Nat] means (F() . $1) = (G() . $1);

      

       A8: for n st P[n] holds P[( succ n)]

      proof

        let n;

        assume (F() . n) = (G() . n);

        then

         A9: P[n, (F() . n), (G() . ( succ n))] by A6;

        P[n, (F() . n), (F() . ( succ n))] by A3;

        hence thesis by A7, A9;

      end;

      

       A10: P[ 0 ] by A2, A5;

      for n holds P[n]

      proof

        let n;

        thus thesis from OmegaInd( A10, A8);

      end;

      then for x be object st x in omega holds (F() . x) = (G() . x);

      hence thesis by A1, A4, FUNCT_1: 2;

    end;

    scheme :: ORDINAL2:sch20

    LambdaRecUn { A() -> set , F( set, set) -> set , F,G() -> Function } :

F() = G()

      provided

       A1: ( dom F()) = omega

       and

       A2: (F() . 0 ) = A()

       and

       A3: for n holds (F() . ( succ n)) = F(n,.)

       and

       A4: ( dom G()) = omega

       and

       A5: (G() . 0 ) = A()

       and

       A6: for n holds (G() . ( succ n)) = F(n,.);

      defpred P[ Nat, set, set] means $3 = F($1,$2);

      

       A7: for n holds P[n, (G() . n), (G() . ( succ n))] by A6;

      

       A8: for n be Nat, x,y1,y2 be set st P[n, x, y1] & P[n, x, y2] holds y1 = y2;

      

       A9: for n holds P[n, (F() . n), (F() . ( succ n))] by A3;

      thus F() = G() from RecUn( A1, A2, A9, A4, A5, A7, A8);

    end;