ordinal5.miz



    begin

    reserve a,b,c,d,e for Ordinal,

m,n for Nat,

f for Ordinal-Sequence,

x for object;

    theorem :: ORDINAL5:1

    

     Th1: a c= ( succ b) implies a c= b or a = ( succ b) by ORDINAL1: 16, ORDINAL1: 21;

    registration

      cluster omega -> limit_ordinal;

      coherence ;

      cluster -> Ordinal-yielding for empty set;

      coherence

      proof

        let f be empty set;

        take 0 ;

        thus thesis;

      end;

    end

    registration

      cluster non empty finite for Sequence;

      existence

      proof

        set x = the set;

        take <%x%>;

        thus thesis;

      end;

    end

    registration

      let f be Sequence;

      let g be non empty Sequence;

      cluster (f ^ g) -> non empty;

      coherence

      proof

        (( dom f) +^ ( dom g)) <> 0 by ORDINAL3: 26;

        then ( dom (f ^ g)) <> 0 by ORDINAL4:def 1;

        hence thesis;

      end;

      cluster (g ^ f) -> non empty;

      coherence

      proof

        (( dom g) +^ ( dom f)) <> 0 by ORDINAL3: 26;

        then ( dom (g ^ f)) <> 0 by ORDINAL4:def 1;

        hence thesis;

      end;

    end

    reserve S,S1,S2 for Sequence;

    theorem :: ORDINAL5:2

    

     Th2: ( dom S) = (a +^ b) implies ex S1, S2 st S = (S1 ^ S2) & ( dom S1) = a & ( dom S2) = b

    proof

      assume

       A1: ( dom S) = (a +^ b);

      set S1 = (S | a);

      

       A2: a c= (a +^ b) by ORDINAL3: 24;

      then

       A3: ( dom S1) = a by A1, RELAT_1: 62;

      deffunc F( Ordinal) = (S . (a +^ $1));

      consider S2 such that

       A4: ( dom S2) = b & for c st c in b holds (S2 . c) = F(c) from ORDINAL2:sch 2;

      take S1, S2;

      set s = (S1 ^ S2);

      

       A5: ( dom S) = ( dom s) by A1, A3, A4, ORDINAL4:def 1;

      now

        let x be object;

        assume

         A6: x in ( dom S);

        then

        reconsider z = x as Ordinal;

        per cases by A1, A6, ORDINAL3: 38;

          suppose

           A7: z in a;

          

          hence (S . x) = (S1 . z) by FUNCT_1: 49

          .= (s . x) by A7, A3, ORDINAL4:def 1;

        end;

          suppose ex c st c in b & z = (a +^ c);

          then

          consider c such that

           A8: c in b & z = (a +^ c);

          

          thus (S . x) = (S2 . c) by A4, A8

          .= (s . x) by A8, A3, A4, ORDINAL4:def 1;

        end;

      end;

      hence thesis by A2, A4, A5, A1, FUNCT_1: 2, RELAT_1: 62;

    end;

    theorem :: ORDINAL5:3

    

     Th3: ( rng S1) c= ( rng (S1 ^ S2)) & ( rng S2) c= ( rng (S1 ^ S2))

    proof

      set q = (S1 ^ S2);

      

       A1: ( dom q) = (( dom S1) +^ ( dom S2)) by ORDINAL4:def 1;

      then

       A2: ( dom S1) c= ( dom q) by ORDINAL3: 24;

      thus ( rng S1) c= ( rng (S1 ^ S2))

      proof

        let x be object;

        assume x in ( rng S1);

        then

        consider z be object such that

         A3: z in ( dom S1) & x = (S1 . z) by FUNCT_1:def 3;

        reconsider z as Ordinal by A3;

        (q . z) = x & z in ( dom q) by A3, A2, ORDINAL4:def 1;

        hence thesis by FUNCT_1:def 3;

      end;

      let x be object;

      assume x in ( rng S2);

      then

      consider z be object such that

       A4: z in ( dom S2) & x = (S2 . z) by FUNCT_1:def 3;

      reconsider z as Ordinal by A4;

      (q . (( dom S1) +^ z)) = x & (( dom S1) +^ z) in ( dom q) by A1, A4, ORDINAL3: 17, ORDINAL4:def 1;

      hence thesis by FUNCT_1:def 3;

    end;

    theorem :: ORDINAL5:4

    

     Th4: (S1 ^ S2) is Ordinal-yielding implies S1 is Ordinal-yielding & S2 is Ordinal-yielding

    proof

      given a such that

       A1: ( rng (S1 ^ S2)) c= a;

      thus S1 is Ordinal-yielding

      proof

        take a;

        ( rng S1) c= ( rng (S1 ^ S2)) by Th3;

        hence thesis by A1;

      end;

      take a;

      ( rng S2) c= ( rng (S1 ^ S2)) by Th3;

      hence thesis by A1;

    end;

    definition

      let f be Sequence;

      :: ORDINAL5:def1

      attr f is decreasing means for a, b st a in b & b in ( dom f) holds (f . b) in (f . a);

      :: ORDINAL5:def2

      attr f is non-decreasing means

      : Def2: for a, b st a in b & b in ( dom f) holds (f . a) c= (f . b);

      :: ORDINAL5:def3

      attr f is non-increasing means for a, b st a in b & b in ( dom f) holds (f . b) c= (f . a);

    end

    registration

      cluster increasing -> non-decreasing for Ordinal-Sequence;

      coherence

      proof

        let f be Ordinal-Sequence such that

         A1: for a, b st a in b & b in ( dom f) holds (f . a) in (f . b);

        let a, b;

        (f . a) in (f . b) implies (f . a) c= (f . b) by ORDINAL1:def 2;

        hence thesis by A1;

      end;

      cluster decreasing -> non-increasing for Ordinal-Sequence;

      coherence by ORDINAL1:def 2;

    end

    theorem :: ORDINAL5:5

    

     Th5: for f be Sequence holds f is infinite iff omega c= ( dom f)

    proof

      let f be Sequence;

      f is infinite iff ( dom f) is infinite by FINSET_1: 10;

      hence thesis by CARD_3: 85;

    end;

    registration

      cluster decreasing -> finite for Sequence;

      coherence

      proof

        let f be Sequence such that

         A1: for a, b st a in b & b in ( dom f) holds (f . b) in (f . a);

        set X = (f .: omega );

        assume f is infinite;

        then

         A2: 0 in omega & omega c= ( dom f) by Th5;

        then (f . 0 ) in X by FUNCT_1:def 6;

        then

        consider x be set such that

         A3: x in X & X misses x by XREGULAR: 1;

        consider a be object such that

         A4: a in ( dom f) & a in omega & x = (f . a) by A3, FUNCT_1:def 6;

        reconsider a as Ordinal by A4;

        

         A5: ( succ a) in omega by A4, ORDINAL1: 28;

        then a in ( succ a) & ( succ a) in ( dom f) by A2, ORDINAL1: 6;

        then (f . ( succ a)) in x & (f . ( succ a)) in X by A1, A4, A5, FUNCT_1:def 6;

        hence thesis by A3, XBOOLE_0: 3;

      end;

      cluster -> decreasing increasing for empty set;

      coherence

      proof

        let e be empty set;

        thus e is decreasing;

        let a;

        thus thesis;

      end;

    end

    registration

      let a;

      cluster <%a%> -> Ordinal-yielding;

      coherence

      proof

        take ( succ a);

        let x be object;

        assume x in ( rng <%a%>);

        then x in {a} by AFINSQ_1: 33;

        then x = a by TARSKI:def 1;

        hence thesis by ORDINAL1: 6;

      end;

    end

    registration

      let a;

      cluster <%a%> -> decreasing increasing;

      coherence

      proof

        set f = <%a%>;

        

         A1: ( dom <%a%>) = 1 & ( <%a%> . 0 ) = a by AFINSQ_1:def 4;

        hence for c, b st c in b & b in ( dom f) holds (f . b) in (f . c) by ORDINAL3: 15, TARSKI:def 1;

        let c, b;

        thus thesis by A1, ORDINAL3: 15, TARSKI:def 1;

      end;

    end

    registration

      cluster decreasing increasing non-decreasing non-increasing finite non empty for Ordinal-Sequence;

      existence

      proof

        set a = the Ordinal;

        take <%a%>;

        thus thesis;

      end;

    end

    theorem :: ORDINAL5:6

    

     Th6: for f be non-decreasing Ordinal-Sequence st ( dom f) is non empty holds ( Union f) is_limes_of f

    proof

      let f be non-decreasing Ordinal-Sequence such that

       A1: ( dom f) is non empty;

      set a0 = the Element of ( dom f);

      per cases ;

        case

         A2: ( Union f) = 0 ;

        take a0;

        thus a0 in ( dom f) by A1;

        let c;

        assume a0 c= c & c in ( dom f);

        then (f . c) in ( rng f) by FUNCT_1:def 3;

        hence (f . c) = 0 by A2, ORDERS_1: 6;

      end;

        case ( Union f) <> 0 ;

        let b, c;

        assume

         A3: b in ( Union f) & ( Union f) in c;

        then

        consider x be object such that

         A4: x in ( dom f) & b in (f . x) by CARD_5: 2;

        reconsider x as Ordinal by A4;

        take x;

        thus x in ( dom f) by A4;

        let E be Ordinal;

        assume

         A5: x c= E & E in ( dom f);

        then x = E or x c< E;

        then x = E or x in E by ORDINAL1: 11;

        then (f . x) c= (f . E) by A5, Def2;

        hence b in (f . E) by A4;

        (f . E) in ( rng f) by A5, FUNCT_1:def 3;

        then (f . E) c= ( Union f) by ZFMISC_1: 74;

        hence (f . E) in c by A3, ORDINAL1: 12;

      end;

    end;

    theorem :: ORDINAL5:7

    a in b implies (n *^ ( exp ( omega ,a))) in ( exp ( omega ,b))

    proof

      assume a in b;

      then ( succ a) c= b by ORDINAL1: 21;

      then

       A1: ( exp ( omega ,( succ a))) c= ( exp ( omega ,b)) by ORDINAL4: 27;

      

       A2: ( exp ( omega ,( succ a))) = ( omega *^ ( exp ( omega ,a))) by ORDINAL2: 44;

      n in omega by ORDINAL1:def 12;

      then (n *^ ( exp ( omega ,a))) in ( omega *^ ( exp ( omega ,a))) by ORDINAL3: 19, ORDINAL4: 22;

      hence thesis by A1, A2;

    end;

    theorem :: ORDINAL5:8

    

     Th8: 0 in a & (for b st b in ( dom f) holds (f . b) = ( exp (a,b))) implies f is non-decreasing

    proof

      assume

       A1: 0 in a & for b st b in ( dom f) holds (f . b) = ( exp (a,b));

      let b, d;

      assume

       A2: b in d & d in ( dom f);

      then b in ( dom f) by ORDINAL1: 10;

      then b c= d & (f . b) = ( exp (a,b)) & (f . d) = ( exp (a,d)) by A1, A2, ORDINAL1:def 2;

      hence thesis by A1, ORDINAL4: 27;

    end;

    theorem :: ORDINAL5:9

    

     Th9: a is limit_ordinal & 0 in b implies ( exp (a,b)) is limit_ordinal

    proof

      assume

       A1: a is limit_ordinal & 0 in b;

      per cases by ORDINAL3: 8;

        suppose a = 0 ;

        hence thesis by A1, ORDINAL4: 20;

      end;

        suppose

         A2: 0 in a;

        defpred P[ Ordinal] means 0 in $1 implies ( exp (a,$1)) is limit_ordinal;

        

         A3: P[ 0 ];

        

         A4: P[c] implies P[( succ c)]

        proof

          ( exp (a,( succ c))) = (a *^ ( exp (a,c))) by ORDINAL2: 44;

          hence thesis by A1, ORDINAL3: 40;

        end;

        

         A5: c <> 0 & c is limit_ordinal & (for b st b in c holds P[b]) implies P[c]

        proof

          assume that

           A6: c <> 0 & c is limit_ordinal and

           A7: for b st b in c holds P[b];

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

          consider f such that

           A8: ( dom f) = c & for b st b in c holds (f . b) = F(b) from ORDINAL2:sch 3;

          

           A9: ( exp (a,c)) = ( lim f) by A6, A8, ORDINAL2: 45;

          f is non-decreasing by A2, A8, Th8;

          then ( Union f) is_limes_of f by A6, A8, Th6;

          then

           A10: ( exp (a,c)) = ( Union f) by A9, ORDINAL2:def 10;

          for d st d in ( exp (a,c)) holds ( succ d) in ( exp (a,c))

          proof

            let d;

            assume d in ( exp (a,c));

            then

            consider b be object such that

             A11: b in ( dom f) & d in (f . b) by A10, CARD_5: 2;

            reconsider b as Ordinal by A11;

            

             A12: ( succ b) in ( dom f) by A6, A8, A11, ORDINAL1: 28;

            then

             A13: (f . b) = F(b) & (f . ( succ b)) = F(succ) & P[( succ b)] by A7, A8, A11;

             F(b) c= F(succ) by A2, ORDINAL3: 1, ORDINAL4: 27;

            then ( succ d) in (f . ( succ b)) by A13, A11, ORDINAL1: 28, ORDINAL3: 8;

            hence ( succ d) in ( exp (a,c)) by A10, A12, CARD_5: 2;

          end;

          hence P[c] by ORDINAL1: 28;

        end;

         P[c] from ORDINAL2:sch 1( A3, A4, A5);

        hence thesis by A1;

      end;

    end;

    theorem :: ORDINAL5:10

    1 in a & (for b st b in ( dom f) holds (f . b) = ( exp (a,b))) implies f is increasing

    proof

      assume

       A1: 1 in a & for b st b in ( dom f) holds (f . b) = ( exp (a,b));

      let b, d;

      assume

       A2: b in d & d in ( dom f);

      then (f . b) = ( exp (a,b)) & (f . d) = ( exp (a,d)) by A1, ORDINAL1: 10;

      hence thesis by A1, A2, ORDINAL4: 24;

    end;

    theorem :: ORDINAL5:11

    

     Th11: 0 in a & b is non empty limit_ordinal implies (x in ( exp (a,b)) iff ex c st c in b & x in ( exp (a,c)))

    proof

      assume

       A1: 0 in a & b is non empty limit_ordinal;

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

      consider f such that

       A2: ( dom f) = b & for c st c in b holds (f . c) = F(c) from ORDINAL2:sch 3;

      f is non-decreasing by A1, A2, Th8;

      then ( Union f) is_limes_of f by A1, A2, Th6;

      

      then

       A3: ( Union f) = ( lim f) by ORDINAL2:def 10

      .= ( exp (a,b)) by A1, A2, ORDINAL2: 45;

      hereby

        assume x in ( exp (a,b));

        then

        consider c be object such that

         A4: c in ( dom f) & x in (f . c) by A3, CARD_5: 2;

        reconsider c as Ordinal by A4;

        take c;

        thus c in b by A2, A4;

        thus x in ( exp (a,c)) by A2, A4;

      end;

      given c such that

       A5: c in b & x in ( exp (a,c));

      (f . c) = F(c) by A2, A5;

      hence x in ( exp (a,b)) by A2, A3, A5, CARD_5: 2;

    end;

    theorem :: ORDINAL5:12

    

     Th12: 0 in a & ( exp (a,b)) in ( exp (a,c)) implies b in c

    proof

      assume

       A1: 0 in a & ( exp (a,b)) in ( exp (a,c));

      assume not b in c;

      then ( exp (a,c)) c= ( exp (a,b)) by A1, ORDINAL1: 16, ORDINAL4: 27;

      then ( exp (a,b)) in ( exp (a,b)) by A1;

      hence thesis;

    end;

    begin

    definition

      let a,b be Ordinal;

      :: ORDINAL5:def4

      func a |^|^ b -> Ordinal means

      : Def4: ex phi be Ordinal-Sequence st it = ( last phi) & ( dom phi) = ( succ b) & (phi . {} ) = 1 & (for c be Ordinal st ( succ c) in ( succ b) holds (phi . ( succ c)) = ( exp (a,(phi . c)))) & for c be Ordinal st c in ( succ b) & c <> {} & c is limit_ordinal holds (phi . c) = ( lim (phi | c));

      correctness

      proof

        deffunc C( Ordinal, Ordinal) = ( exp (a,$2));

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

        (ex F be Ordinal, fi be Ordinal-Sequence st F = ( last fi) & ( dom fi) = ( succ b) & (fi . 0 ) = 1 & (for c be Ordinal st ( succ c) in ( succ b) holds (fi . ( succ c)) = C(c,.)) & for c be Ordinal st c in ( succ b) & c <> 0 & c is limit_ordinal holds (fi . c) = D(c,|)) & for A1,A2 be Ordinal st (ex fi be Ordinal-Sequence st A1 = ( last fi) & ( dom fi) = ( succ b) & (fi . 0 ) = 1 & (for C be Ordinal st ( succ C) in ( succ b) holds (fi . ( succ C)) = C(C,.)) & for C be Ordinal st C in ( succ b) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|)) & (ex fi be Ordinal-Sequence st A2 = ( last fi) & ( dom fi) = ( succ b) & (fi . 0 ) = 1 & (for C be Ordinal st ( succ C) in ( succ b) holds (fi . ( succ C)) = C(C,.)) & for C be Ordinal st C in ( succ b) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|)) holds A1 = A2 from ORDINAL2:sch 13;

        hence thesis;

      end;

    end

    theorem :: ORDINAL5:13

    

     Th13: (a |^|^ 0 ) = 1

    proof

      deffunc F( Ordinal) = (a |^|^ $1);

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

      deffunc C( Ordinal, Ordinal) = ( exp (a,$2));

      

       A1: for b, c holds c = F(b) iff ex fi be Ordinal-Sequence 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 Def4;

      thus F(0) = 1 from ORDINAL2:sch 14( A1);

    end;

    theorem :: ORDINAL5:14

    

     Th14: (a |^|^ ( succ b)) = ( exp (a,(a |^|^ b)))

    proof

      deffunc F( Ordinal) = (a |^|^ $1);

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

      deffunc C( Ordinal, Ordinal) = ( exp (a,$2));

      

       A1: for b, c holds c = F(b) iff ex fi be Ordinal-Sequence 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 Def4;

      for b holds F(succ) = C(b,F) from ORDINAL2:sch 15( A1);

      hence thesis;

    end;

    theorem :: ORDINAL5:15

    

     Th15: b <> 0 & b is limit_ordinal implies for phi be Ordinal-Sequence st ( dom phi) = b & for c st c in b holds (phi . c) = (a |^|^ c) holds (a |^|^ b) = ( lim phi)

    proof

      assume

       A1: b <> 0 & b is limit_ordinal;

      deffunc F( Ordinal) = (a |^|^ $1);

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

      deffunc C( Ordinal, Ordinal) = ( exp (a,$2));

      let fi be Ordinal-Sequence 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 be Ordinal-Sequence 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 Def4;

      thus F(b) = D(b,fi) from ORDINAL2:sch 16( A4, A1, A2, A3);

    end;

    theorem :: ORDINAL5:16

    

     Th16: (a |^|^ 1) = a

    proof

      ( 0 + 1) = ( succ 0 );

      

      hence (a |^|^ 1) = ( exp (a,(a |^|^ 0 ))) by Th14

      .= ( exp (a,1)) by Th13

      .= a by ORDINAL2: 46;

    end;

    theorem :: ORDINAL5:17

    

     Th17: (1 |^|^ a) = 1

    proof

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

      

       A1: P[ 0 ] by Th13;

      

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

      proof

        let A be Ordinal;

        assume P[A];

        

        hence (1 |^|^ ( succ A)) = ( exp (1,1)) by Th14

        .= 1 by ORDINAL2: 46;

      end;

      

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

      proof

        let A be Ordinal such that

         A4: A <> 0 & A is limit_ordinal and

         A5: for B be Ordinal st B in A holds (1 |^|^ B) = 1;

        deffunc F( Ordinal) = (1 |^|^ $1);

        consider fi be Ordinal-Sequence such that

         A6: ( dom fi) = A & for B be Ordinal st B in A holds (fi . B) = F(B) from ORDINAL2:sch 3;

        

         A7: (1 |^|^ A) = ( lim fi) by A4, A6, Th15;

        

         A8: ( rng fi) c= {1}

        proof

          let x be object;

          assume x in ( rng fi);

          then

          consider y be object such that

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

          reconsider y as Ordinal by A9;

          x = (1 |^|^ y) by A6, A9

          .= 1 by A5, A6, A9;

          hence x in {1} by TARSKI:def 1;

        end;

        now

          thus {} <> 1;

          let b, c such that

           A10: b in 1 & 1 in c;

          set x = the Element of A;

          reconsider x as Ordinal;

          take D = x;

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

          let E be Ordinal;

          assume D c= E & E in ( dom fi);

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

          hence b in (fi . E) & (fi . E) in c by A8, A10, TARSKI:def 1;

        end;

        then 1 is_limes_of fi by ORDINAL2:def 9;

        hence (1 |^|^ A) = 1 by A7, ORDINAL2:def 10;

      end;

      for a holds P[a] from ORDINAL2:sch 1( A1, A2, A3);

      hence thesis;

    end;

    theorem :: ORDINAL5:18

    

     Th18: (a |^|^ 2) = ( exp (a,a))

    proof

      2 = ( succ 1);

      

      hence (a |^|^ 2) = ( exp (a,(a |^|^ 1))) by Th14

      .= ( exp (a,a)) by Th16;

    end;

    theorem :: ORDINAL5:19

    (a |^|^ 3) = ( exp (a,( exp (a,a))))

    proof

      3 = ( succ 2);

      

      hence (a |^|^ 3) = ( exp (a,(a |^|^ 2))) by Th14

      .= ( exp (a,( exp (a,a)))) by Th18;

    end;

    theorem :: ORDINAL5:20

    for n be Nat holds ( 0 |^|^ (2 * n)) = 1 & ( 0 |^|^ ((2 * n) + 1)) = 0

    proof

      defpred P[ Nat] means ( 0 |^|^ (2 * $1)) = 1 & ( 0 |^|^ ((2 * $1) + 1)) = 0 ;

      

       A1: P[ 0 ] by Th13, Th16;

       A2:

      now

        let n be Nat;

        assume

         A3: P[n];

        thus P[(n + 1)]

        proof

          

          thus

           A4: ( 0 |^|^ (2 * (n + 1))) = ( 0 |^|^ ( Segm (((2 * n) + 1) + 1)))

          .= ( 0 |^|^ ( succ ( Segm ((2 * n) + 1)))) by NAT_1: 38

          .= ( exp ( 0 , 0 )) by A3, Th14

          .= 1 by ORDINAL2: 43;

          

          thus ( 0 |^|^ ((2 * (n + 1)) + 1)) = ( 0 |^|^ ( Segm ((2 * (n + 1)) + 1)))

          .= ( 0 |^|^ ( succ ( Segm (2 * (n + 1))))) by NAT_1: 38

          .= ( exp ( 0 ,1)) by A4, Th14

          .= 0 by ORDINAL2: 46;

        end;

      end;

      thus for n be Nat holds P[n] from NAT_1:sch 2( A1, A2);

    end;

    theorem :: ORDINAL5:21

    

     Th21: a c= b & 0 in c implies (c |^|^ a) c= (c |^|^ b)

    proof

      assume that

       A1: a c= b and

       A2: 0 in c;

      ( succ 0 ) c= c & ( succ 0 ) = ( 0 + 1) by A2, ORDINAL1: 21;

      then

       A3: 1 c< c or 1 = c;

      per cases by A3, ORDINAL1: 11;

        suppose c = 1;

        then (c |^|^ a) = 1 & (c |^|^ b) = 1 by Th17;

        hence thesis;

      end;

        suppose

         A4: 1 in c;

        defpred H[ Ordinal] means for a, b st a c= b & b c= $1 holds (c |^|^ a) c= (c |^|^ b);

        

         A5: H[ 0 ]

        proof

          let a, b;

          assume

           A6: a c= b & b c= 0 ;

          then b = {} ;

          hence thesis by A6;

        end;

         A7:

        now

          let d such that

           A8: H[d];

          (c |^|^ ( succ d)) = ( exp (c,(c |^|^ d))) by Th14;

          then

           A9: (c |^|^ d) c= (c |^|^ ( succ d)) by A4, ORDINAL4: 32;

          thus H[( succ d)]

          proof

            let a, b such that

             A10: a c= b & b c= ( succ d);

            

             A11: a c= ( succ d) by A10;

            per cases by A10, A11, Th1;

              suppose b c= d;

              hence thesis by A8, A10;

            end;

              suppose b = ( succ d) & a = ( succ d);

              hence thesis;

            end;

              suppose

               A12: b = ( succ d) & a c= d;

              then (c |^|^ a) c= (c |^|^ d) by A8;

              hence thesis by A9, A12;

            end;

          end;

        end;

         A13:

        now

          let d such that

           A14: d <> 0 & d is limit_ordinal and

           A15: for e st e in d holds H[e];

          deffunc E( Ordinal) = (c |^|^ $1);

          consider f be Ordinal-Sequence such that

           A16: ( dom f) = d & for e st e in d holds (f . e) = E(e) from ORDINAL2:sch 3;

          f is non-decreasing

          proof

            let a, b;

            assume

             A17: a in b & b in ( dom f);

            then a c= b & H[b] by A15, A16, ORDINAL1:def 2;

            then (c |^|^ a) c= (c |^|^ b) & a in d & (f . b) = E(b) by A16, A17, ORDINAL1: 12;

            hence thesis by A16;

          end;

          then

           A18: ( Union f) is_limes_of f by A14, A16, Th6;

          (c |^|^ d) = ( lim f) by A14, A16, Th15;

          then

           A19: (c |^|^ d) = ( Union f) by A18, ORDINAL2:def 10;

          thus H[d]

          proof

            let a, b;

            assume

             A20: a c= b & b c= d;

            then

             A21: (b c< d or b = d) & (a c< b or a = b);

            per cases by A21, ORDINAL1: 11;

              suppose b in d;

              hence E(a) c= E(b) by A20, A15;

            end;

              suppose

               A22: b = d & a in d;

              then (f . a) in ( rng f) & (f . a) = E(a) by A16, FUNCT_1:def 3;

              hence E(a) c= E(b) by A19, A22, ZFMISC_1: 74;

            end;

              suppose b = d & a = d;

              hence E(a) c= E(b);

            end;

          end;

        end;

        for b holds H[b] from ORDINAL2:sch 1( A5, A7, A13);

        hence thesis by A1;

      end;

    end;

    theorem :: ORDINAL5:22

     0 in a & (for b st b in ( dom f) holds (f . b) = (a |^|^ b)) implies f is non-decreasing

    proof

      assume that

       A1: 0 in a and

       A2: for b st b in ( dom f) holds (f . b) = (a |^|^ b);

      let b, c;

      assume

       A3: b in c & c in ( dom f);

      then b c= c by ORDINAL1:def 2;

      then (a |^|^ b) c= (a |^|^ c) & (a |^|^ c) = (f . c) by A1, A2, A3, Th21;

      hence (f . b) c= (f . c) by A2, A3, ORDINAL1: 10;

    end;

    theorem :: ORDINAL5:23

    

     Th23: 0 in a & 0 in b implies a c= (a |^|^ b)

    proof

      assume

       A1: 0 in a & 0 in b;

      defpred J[ Ordinal] means 0 in $1 implies a c= (a |^|^ $1);

      

       A2: J[ 0 ];

       A3:

      now

        let b;

        assume

         A4: J[b];

        

         A5: (a |^|^ ( succ b)) = ( exp (a,(a |^|^ b))) by Th14;

        

         A6: ( succ 0 ) = ( 0 + 1);

        thus J[( succ b)]

        proof

          per cases by ORDINAL3: 8;

            suppose 0 in b;

            then 1 c= (a |^|^ b) by A6, A1, A4, ORDINAL1: 21;

            then ( exp (a,1)) c= ( exp (a,(a |^|^ b))) by A1, ORDINAL4: 27;

            hence thesis by A5, ORDINAL2: 46;

          end;

            suppose b = 0 ;

            then (a |^|^ b) = 1 by Th13;

            hence thesis by A5, ORDINAL2: 46;

          end;

        end;

      end;

       A7:

      now

        let c such that

         A8: c <> 0 & c is limit_ordinal & for b st b in c holds J[b];

        deffunc F( Ordinal) = (a |^|^ $1);

        consider phi be Ordinal-Sequence such that

         A9: ( dom phi) = c & for b st b in c holds (phi . b) = F(b) from ORDINAL2:sch 3;

        phi is non-decreasing

        proof

          let e, b;

          assume

           A10: e in b & b in ( dom phi);

          then

           A11: (phi . b) = F(b) & e in c by A9, ORDINAL1: 10;

          then (phi . e) = F(e) & e c= b by A9, A10, ORDINAL1:def 2;

          hence thesis by A1, A11, Th21;

        end;

        then

         A12: ( Union phi) is_limes_of phi by A8, A9, Th6;

        ( lim phi) = F(c) by A8, A9, Th15;

        then

         A13: F(c) = ( Union phi) by A12, ORDINAL2:def 10;

        thus J[c]

        proof

          assume 0 in c;

          then ( succ 0 ) in c by A8, ORDINAL1: 28;

          then (phi . 1) in ( rng phi) & (phi . 1) = F() & F() = a by A9, Th16, FUNCT_1:def 3;

          hence thesis by A13, ZFMISC_1: 74;

        end;

      end;

      for b holds J[b] from ORDINAL2:sch 1( A2, A3, A7);

      hence thesis by A1;

    end;

    theorem :: ORDINAL5:24

    

     Th24: 1 in a & m < n implies (a |^|^ m) in (a |^|^ n)

    proof

      assume

       A1: 1 in a & m < n;

      then (m + 1) <= n by NAT_1: 13;

      then

      consider k be Nat such that

       A2: n = ((m + 1) + k) by NAT_1: 10;

      defpred Q[ Nat] means (a |^|^ $1) in (a |^|^ ($1 + 1));

      defpred P[ Nat] means (a |^|^ m) in (a |^|^ ((m + 1) + $1));

      (a |^|^ 0 ) = 1 by Th13;

      then

       A3: Q[ 0 ] by A1, Th16;

       A4:

      now

        let n;

        assume

         A5: Q[n];

        ( succ ( Segm n)) = ( Segm (n + 1)) & ( succ ( Segm (n + 1))) = ( Segm ((n + 1) + 1)) by NAT_1: 38;

        then (a |^|^ (n + 1)) = ( exp (a,(a |^|^ n))) & (a |^|^ ((n + 1) + 1)) = ( exp (a,(a |^|^ (n + 1)))) by Th14;

        hence Q[(n + 1)] by A5, A1, ORDINAL4: 24;

      end;

      

       A6: for n holds Q[n] from NAT_1:sch 2( A3, A4);

      then

       A7: P[ 0 ];

       A8:

      now

        let k be Nat;

        assume

         A9: P[k];

        (a |^|^ ((m + 1) + k)) in (a |^|^ (((m + 1) + k) + 1)) by A6;

        hence P[(k + 1)] by A9, ORDINAL1: 10;

      end;

      for k be Nat holds P[k] from NAT_1:sch 2( A7, A8);

      hence thesis by A2;

    end;

    theorem :: ORDINAL5:25

    

     Th25: 1 in a & ( dom f) c= omega & (for b st b in ( dom f) holds (f . b) = (a |^|^ b)) implies f is increasing

    proof

      assume that

       A1: 1 in a and

       A2: ( dom f) c= omega and

       A3: for n be Ordinal st n in ( dom f) holds (f . n) = (a |^|^ n);

      let b, c;

      assume

       A4: b in c & c in ( dom f);

      then

       A5: b in ( dom f) by ORDINAL1: 10;

      reconsider b, c as Element of omega by A2, A4, ORDINAL1: 10;

      b in ( Segm c) by A4;

      then (f . b) = (a |^|^ b) & (f . c) = (a |^|^ c) & b < c by A3, A4, A5, NAT_1: 44;

      hence thesis by A1, Th24;

    end;

    theorem :: ORDINAL5:26

    

     Th26: 1 in a & 1 in b implies a in (a |^|^ b)

    proof

      assume

       A1: 1 in a;

      assume 1 in b;

      then

       A2: ( succ 1) c= b by ORDINAL1: 21;

       0 in ( Segm 1) by NAT_1: 44;

      then 0 in a by A1, ORDINAL1: 10;

      then (a |^|^ 1) in (a |^|^ 2) & (a |^|^ 2) c= (a |^|^ b) by A1, A2, Th21, Th24;

      then (a |^|^ 1) in (a |^|^ b);

      hence a in (a |^|^ b) by Th16;

    end;

    theorem :: ORDINAL5:27

    

     Th27: for n,k be Nat holds ( exp (n,k)) = (n |^ k)

    proof

      let n be Nat;

      defpred P[ Nat] means ( exp (n,$1)) = (n |^ $1);

      ( exp (n, 0 )) = 1 by ORDINAL2: 43;

      then

       A1: P[ 0 ] by NEWTON: 4;

       A2:

      now

        let k be Nat such that

         A3: P[k];

        reconsider n9 = n, nk = (n |^ k) as Element of NAT by ORDINAL1:def 12;

        ( Segm (k + 1)) = ( succ ( Segm k)) by NAT_1: 38;

        

        then ( exp (n,(k + 1))) = (n *^ ( exp (n,k))) by ORDINAL2: 44

        .= (n9 * nk) by A3, CARD_2: 37;

        hence P[(k + 1)] by NEWTON: 6;

      end;

      thus for k be Nat holds P[k] from NAT_1:sch 2( A1, A2);

    end;

    registration

      let n,k be Nat;

      cluster ( exp (n,k)) -> natural;

      coherence

      proof

        ( exp (n,k)) = (n |^ k) by Th27;

        hence thesis;

      end;

    end

    registration

      let n,k be Nat;

      cluster (n |^|^ k) -> natural;

      coherence

      proof

        defpred O[ Nat] means (n |^|^ $1) is natural;

        

         A1: O[ 0 ] by Th13;

         A2:

        now

          let k be Nat;

          assume O[k];

          then

          reconsider nk = (n |^|^ k) as Nat;

          ( Segm (k + 1)) = ( succ ( Segm k)) by NAT_1: 38;

          then (n |^|^ (k + 1)) = ( exp (n,nk)) by Th14;

          hence O[(k + 1)];

        end;

        for k be Nat holds O[k] from NAT_1:sch 2( A1, A2);

        hence thesis;

      end;

    end

    theorem :: ORDINAL5:28

    

     Th28: for n,k be Nat st n > 1 holds (n |^|^ k) > k

    proof

      let n,k be Nat such that

       A1: n > 1;

      defpred H[ Nat] means (n |^|^ $1) > $1;

      

       A2: H[ 0 ] by Th13;

       A3:

      now

        let k be Nat such that

         A4: H[k];

        ( succ ( Segm k)) = ( Segm (k + 1)) by NAT_1: 38;

        

        then (n |^|^ (k + 1)) = ( exp (n,(n |^|^ k))) by Th14

        .= (n |^ (n |^|^ k)) by Th27;

        then

         A5: (n |^|^ (k + 1)) > (n |^ k) by A1, A4, PEPIN: 66;

        (n |^ k) > k by A1, NAT_4: 3;

        then (n |^ k) >= (k + 1) by NAT_1: 13;

        hence H[(k + 1)] by A5, XXREAL_0: 2;

      end;

      for k be Nat holds H[k] from NAT_1:sch 2( A2, A3);

      hence thesis;

    end;

    theorem :: ORDINAL5:29

    for n be Nat st n > 1 holds (n |^|^ omega ) = omega

    proof

      let n be Nat such that

       A1: n > 1;

      deffunc F( Ordinal) = (n |^|^ $1);

      consider phi be Ordinal-Sequence such that

       A2: ( dom phi) = omega & for b st b in omega holds (phi . b) = F(b) from ORDINAL2:sch 3;

      

       A3: ( rng phi) c= omega

      proof

        let x be object;

        assume x in ( rng phi);

        then

        consider a be object such that

         A4: a in ( dom phi) & x = (phi . a) by FUNCT_1:def 3;

        reconsider a as Element of omega by A2, A4;

        x = (n |^|^ a) by A2, A4;

        hence thesis by ORDINAL1:def 12;

      end;

      

       A5: (n |^|^ omega ) = ( lim phi) by A2, Th15;

      now

        thus {} <> omega ;

        let b, c such that

         A6: b in omega & omega in c;

        reconsider x = b as Element of omega by A6;

        take D = (n |^|^ x);

        thus D in ( dom phi) by A2, ORDINAL1:def 12;

        x < D by A1, Th28;

        then

         A7: b in ( Segm D) by NAT_1: 44;

        let E be Ordinal;

        assume

         A8: D c= E & E in ( dom phi);

        then

        reconsider e = E as Element of omega by A2;

        x in ( Segm e) by A7, A8;

        then x < e & e < (n |^|^ e) by A1, Th28, NAT_1: 44;

        then

         A9: x < (n |^|^ e) & (phi . e) = F(e) by A2, XXREAL_0: 2;

        (phi . E) in ( rng phi) by A8, FUNCT_1:def 3;

        then

        reconsider phiE = (phi . E) as Nat by A3;

        b in ( Segm phiE) by A9, NAT_1: 44;

        hence b in (phi . E);

        (phi . E) in ( rng phi) by A8, FUNCT_1:def 3;

        hence (phi . E) in c by A6, A3, ORDINAL1: 10;

      end;

      then omega is_limes_of phi by ORDINAL2:def 9;

      hence (n |^|^ omega ) = omega by A5, ORDINAL2:def 10;

    end;

    theorem :: ORDINAL5:30

    

     Th30: 1 in a implies (a |^|^ omega ) is limit_ordinal

    proof

      assume

       A1: 1 in a;

      deffunc F( Ordinal) = (a |^|^ $1);

      consider phi be Ordinal-Sequence such that

       A2: ( dom phi) = omega & for b st b in omega holds (phi . b) = F(b) from ORDINAL2:sch 3;

      phi is increasing

      proof

        let b, c;

        assume

         A3: b in c & c in ( dom phi);

        then

        reconsider b, c as Element of NAT by A2, ORDINAL1: 10;

        b in ( Segm c) by A3;

        then b < c by NAT_1: 44;

        then (phi . b) = F(b) & F(b) in F(c) by A1, A2, Th24;

        hence thesis by A2;

      end;

      then ( lim phi) = ( sup phi) & ( sup phi) is limit_ordinal by A2, ORDINAL4: 8, ORDINAL4: 16;

      hence thesis by A2, Th15;

    end;

    theorem :: ORDINAL5:31

    

     Th31: 0 in a implies ( exp (a,(a |^|^ omega ))) = (a |^|^ omega )

    proof

      assume 0 in a;

      then 1 = ( succ 0 ) & ( succ 0 ) c= a by ORDINAL1: 21;

      then

       A1: 1 = a or 1 c< a;

      per cases by A1, ORDINAL1: 11;

        suppose

         A2: a = 1;

        

        hence ( exp (a,(a |^|^ omega ))) = 1 by ORDINAL2: 46

        .= (a |^|^ omega ) by A2, Th17;

      end;

        suppose

         A3: 1 in a;

        deffunc T( Ordinal) = (a |^|^ $1);

        deffunc E( Ordinal) = ( exp (a,$1));

        consider T be Ordinal-Sequence such that

         A4: ( dom T) = omega & for a st a in omega holds (T . a) = T(a) from ORDINAL2:sch 3;

        consider E be Ordinal-Sequence such that

         A5: ( dom E) = (a |^|^ omega ) & for b st b in (a |^|^ omega ) holds (E . b) = E(b) from ORDINAL2:sch 3;

         0 in ( Segm 1) by NAT_1: 44;

        then 0 in a & 0 in omega by A3, ORDINAL1: 10;

        then

         A6: a c= (a |^|^ omega ) by Th23;

        E is increasing Ordinal-Sequence by A3, A5, ORDINAL4: 25;

        then ( lim E) = ( exp (a,(a |^|^ omega ))) & ( Union E) is_limes_of E by A5, A6, Th6, A3, Th30, ORDINAL2: 45;

        then

         A7: ( exp (a,(a |^|^ omega ))) = ( Union E) by ORDINAL2:def 10;

        T is increasing Ordinal-Sequence by A3, A4, Th25;

        then ( lim T) = (a |^|^ omega ) & ( Union T) is_limes_of T by A4, Th15, Th6;

        then

         A8: (a |^|^ omega ) = ( Union T) by ORDINAL2:def 10;

        thus ( exp (a,(a |^|^ omega ))) c= (a |^|^ omega )

        proof

          let x be Ordinal;

          assume x in ( exp (a,(a |^|^ omega )));

          then

          consider b be object such that

           A9: b in ( dom E) & x in (E . b) by A7, CARD_5: 2;

          consider c be object such that

           A10: c in ( dom T) & b in (T . c) by A5, A8, A9, CARD_5: 2;

          reconsider b as Ordinal by A9;

          reconsider c as Element of omega by A4, A10;

          

           A11: ( exp (a,b)) in ( exp (a,(T . c))) by A3, A10, ORDINAL4: 24;

          

           A12: ( succ c) in omega by ORDINAL1:def 12;

          then (E . b) = E(b) & (T . c) = T(c) & (T . ( succ c)) = T(succ) by A9, A4, A5;

          then (E . b) in (T . ( succ c)) by A11, Th14;

          then x in (T . ( succ c)) by A9, ORDINAL1: 10;

          hence thesis by A4, A8, CARD_5: 2, A12;

        end;

        thus (a |^|^ omega ) c= ( exp (a,(a |^|^ omega ))) by A3, ORDINAL4: 32;

      end;

    end;

    theorem :: ORDINAL5:32

     0 in a & omega c= b implies (a |^|^ b) = (a |^|^ omega )

    proof

      assume

       A1: 0 in a;

      assume omega c= b;

      then

       A2: b = ( omega +^ (b -^ omega )) by ORDINAL3:def 5;

      defpred P[ Ordinal] means (a |^|^ ( omega +^ $1)) = (a |^|^ omega );

      

       A3: P[ 0 ] by ORDINAL2: 27;

      

       A4: P[c] implies P[( succ c)]

      proof

        assume P[c];

        then

         A5: ( exp (a,(a |^|^ ( omega +^ c)))) = (a |^|^ omega ) by A1, Th31;

        

        thus (a |^|^ ( omega +^ ( succ c))) = (a |^|^ ( succ ( omega +^ c))) by ORDINAL2: 28

        .= (a |^|^ omega ) by A5, Th14;

      end;

      

       A6: c <> 0 & c is limit_ordinal & (for b st b in c holds P[b]) implies P[c]

      proof

        assume

         A7: c <> 0 & c is limit_ordinal;

        assume

         A8: for b st b in c holds P[b];

        deffunc F( Ordinal) = (a |^|^ $1);

        consider f such that

         A9: ( dom f) = ( omega +^ c) & for b st b in ( omega +^ c) holds (f . b) = F(b) from ORDINAL2:sch 3;

        ( omega +^ c) <> {} & ( omega +^ c) is limit_ordinal by A7, ORDINAL3: 26, ORDINAL3: 29;

        then

         A10: (a |^|^ ( omega +^ c)) = ( lim f) by A9, Th15;

        now

          a c= (a |^|^ omega ) by A1, Th23;

          hence (a |^|^ omega ) <> {} by A1;

          let B,C be Ordinal;

          assume

           A11: B in (a |^|^ omega ) & (a |^|^ omega ) in C;

          take D = omega ;

          ( omega +^ {} qua Ordinal) = omega & {} in c by A7, ORDINAL2: 27, ORDINAL3: 8;

          hence D in ( dom f) by A9, ORDINAL2: 32;

          let E be Ordinal;

          assume

           A12: D c= E & E in ( dom f);

          then (E -^ D) in (( omega +^ c) -^ omega ) by A9, ORDINAL3: 53;

          then (E -^ D) in c by ORDINAL3: 52;

          then P[(E -^ D)] by A8;

          then (a |^|^ omega ) = (a |^|^ E) by A12, ORDINAL3:def 5;

          hence B in (f . E) & (f . E) in C by A9, A11, A12;

        end;

        then (a |^|^ omega ) is_limes_of f by ORDINAL2:def 9;

        hence P[c] by A10, ORDINAL2:def 10;

      end;

       P[c] from ORDINAL2:sch 1( A3, A4, A6);

      hence (a |^|^ b) = (a |^|^ omega ) by A2;

    end;

    begin

    scheme :: ORDINAL5:sch1

    CriticalNumber2 { a() -> Ordinal , f() -> Ordinal-Sequence , phi( Ordinal) -> Ordinal } :

a() c= ( Union f()) & phi(Union) = ( Union f()) & for b st a() c= b & phi(b) = b holds ( Union f()) c= b

      provided

       A1: for a, b st a in b holds phi(a) in phi(b)

       and

       A2: for a st a is non empty limit_ordinal holds for phi be Ordinal-Sequence st ( dom phi) = a & for b st b in a holds (phi . b) = phi(b) holds phi(a) is_limes_of phi

       and

       A3: ( dom f()) = omega & (f() . 0 ) = a()

       and

       A4: for a st a in omega holds (f() . ( succ a)) = phi(.);

      

       A5: a() in ( rng f()) by A3, FUNCT_1:def 3;

      hence a() c= ( Union f()) by ZFMISC_1: 74;

      set phi = f();

       A6:

      now

        defpred P[ Ordinal] means not $1 c= phi($1);

        assume

         A7: ex a st P[a];

        consider a such that

         A8: P[a] and

         A9: for b st P[b] holds a c= b from ORDINAL1:sch 1( A7);

        phi(phi) in phi(a) by A1, A8, ORDINAL1: 16;

        then not phi(a) c= phi(phi) by ORDINAL1: 5;

        hence contradiction by A8, A9;

      end;

      then a() c= phi(a);

      then

       A10: a() c< phi(a) or a() = phi(a);

      per cases by A10, ORDINAL1: 11;

        suppose

         A11: phi(a) = a();

        

         A12: for a be set st a in omega holds (f() . a) = a()

        proof

          let a be set;

          assume a in omega ;

          then

          reconsider a as Element of omega ;

          defpred P[ Nat] means (f() . $1) = a();

          

           A13: P[ 0 ] by A3;

           A14:

          now

            let n be Nat;

            assume

             A15: P[n];

            

             A16: ( Segm (n + 1)) = ( succ ( Segm n)) by NAT_1: 38;

            n in omega by ORDINAL1:def 12;

            then (f() . ( succ n)) = phi(a) by A4, A15;

            hence P[(n + 1)] by A11, A16;

          end;

          for n be Nat holds P[n] from NAT_1:sch 2( A13, A14);

          then P[a];

          hence thesis;

        end;

        ( rng f()) = {a()}

        proof

          thus ( rng f()) c= {a()}

          proof

            let x be object;

            assume x in ( rng f());

            then

            consider a be object such that

             A17: a in ( dom f()) & x = (f() . a) by FUNCT_1:def 3;

            x = a() by A12, A17, A3;

            hence thesis by TARSKI:def 1;

          end;

          thus thesis by A5, ZFMISC_1: 31;

        end;

        then ( Union f()) = a() by ZFMISC_1: 25;

        hence phi(Union) = ( Union f()) & for b st a() c= b & phi(b) = b holds ( Union f()) c= b by A11;

      end;

        suppose

         A18: a() in phi(a);

        deffunc F( Ordinal, Ordinal) = phi($2);

        deffunc G( Ordinal, Sequence) = {} ;

         A19:

        now

          let a such that

           A20: ( succ a) in omega ;

          a in ( succ a) by ORDINAL1: 6;

          hence (phi . ( succ a)) = F(a,.) by A4, A20, ORDINAL1: 10;

        end;

        

         A21: for a st a in omega holds a() c= (phi . a) & (phi . a) in (phi . ( succ a))

        proof

          let a;

          assume a in omega ;

          then

          reconsider a as Element of omega ;

          defpred N[ Nat] means a() c= (phi . $1) & (phi . $1) in (phi . ( succ $1));

          

           A22: N[ 0 ] by A18, A3, A4;

           A23:

          now

            let n be Nat;

            assume

             A24: N[n];

            

             A25: ( Segm (n + 1)) = ( succ ( Segm n)) & ( Segm ((n + 1) + 1)) = ( succ ( Segm (n + 1))) & (n + 1) in omega & ((n + 1) + 1) in omega by NAT_1: 38;

            then (phi . (n + 1)) = phi(.) & (phi . ((n + 1) + 1)) = phi(.) by A19;

            then (phi . n) c= (phi . (n + 1)) & (phi . (n + 1)) in (phi . ((n + 1) + 1)) by A1, A6, A24, A25;

            hence N[(n + 1)] by A24, XBOOLE_1: 1, A25;

          end;

          for n be Nat holds N[n] from NAT_1:sch 2( A22, A23);

          then N[a];

          hence thesis;

        end;

        deffunc phi( Ordinal) = phi($1);

        consider fi be Ordinal-Sequence such that

         A26: ( dom fi) = ( Union phi) & for a st a in ( Union phi) holds (fi . a) = phi(a) from ORDINAL2:sch 3;

        1 = ( succ 0 );

        then (f() . 1) = phi(a) by A3, A4;

        then phi(a) in ( rng phi) by A3, FUNCT_1:def 3;

        then

         A27: phi(a) c= ( Union phi) by ZFMISC_1: 74;

        now

          let c;

          assume c in ( Union phi);

          then

          consider x be object such that

           A28: x in ( dom phi) & c in (phi . x) by CARD_5: 2;

          reconsider x as Element of omega by A3, A28;

          ( succ c) c= (phi . x) & (phi . x) in (phi . ( succ x)) by A21, A28, ORDINAL1: 21;

          then ( succ c) in (phi . ( succ x)) & ( succ x) in omega by ORDINAL1: 12, ORDINAL1:def 12;

          hence ( succ c) in ( Union phi) by A3, CARD_5: 2;

        end;

        then

         A29: ( Union phi) is limit_ordinal by ORDINAL1: 28;

        then

         A30: phi(Union) is_limes_of fi by A2, A26, A27, A18;

        fi is increasing

        proof

          let a, b;

          assume

           A31: a in b & b in ( dom fi);

          then (fi . a) = phi(a) & (fi . b) = phi(b) by A26, ORDINAL1: 10;

          hence thesis by A1, A31;

        end;

        

        then

         A32: ( sup fi) = ( lim fi) by A26, A27, A29, A18, ORDINAL4: 8

        .= phi(Union) by A30, ORDINAL2:def 10;

        thus phi(Union) c= ( Union phi)

        proof

          let x be Ordinal;

          assume

           A33: x in phi(Union);

          reconsider A = x as Ordinal;

          consider b such that

           A34: b in ( rng fi) & A c= b by A32, A33, ORDINAL2: 21;

          consider y be object such that

           A35: y in ( dom fi) & b = (fi . y) by A34, FUNCT_1:def 3;

          reconsider y as Ordinal by A35;

          consider z be object such that

           A36: z in ( dom phi) & y in (phi . z) by A26, A35, CARD_5: 2;

          reconsider z as Ordinal by A36;

          set c = (phi . z);

          ( succ z) in omega by A3, A36, ORDINAL1: 28;

          then (phi . ( succ z)) = phi(c) & (phi . ( succ z)) in ( rng phi) & b = phi(y) by A3, A19, A26, A35, FUNCT_1:def 3;

          then b in phi(c) & phi(c) c= ( Union phi) by A1, A36, ZFMISC_1: 74;

          hence thesis by A34, ORDINAL1: 12;

        end;

        thus ( Union f()) c= phi(Union) by A6;

        let b;

        assume

         A37: a() c= b & phi(b) = b;

        ( rng f()) c= b

        proof

          let x be object;

          assume x in ( rng f());

          then

          consider a be object such that

           A38: a in ( dom f()) & x = (f() . a) by FUNCT_1:def 3;

          reconsider a as Element of omega by A3, A38;

          defpred P[ Nat] means (f() . $1) in b;

          a() <> b by A18, A37;

          then a() c< b by A37;

          then

           A39: P[ 0 ] by A3, ORDINAL1: 11;

           A40:

          now

            let n be Nat;

            assume P[n];

            then phi(.) in b & n in omega by A1, A37, ORDINAL1:def 12;

            then

             A41: (f() . ( succ n)) in b by A4;

            ( Segm (n + 1)) = ( succ ( Segm n)) by NAT_1: 38;

            hence P[(n + 1)] by A41;

          end;

          for n be Nat holds P[n] from NAT_1:sch 2( A39, A40);

          then P[a];

          hence thesis by A38;

        end;

        then ( Union f()) c= ( union b) & ( union b) c= b by ORDINAL2: 5, ZFMISC_1: 77;

        hence ( Union f()) c= b;

      end;

    end;

    scheme :: ORDINAL5:sch2

    CriticalNumber3 { a() -> Ordinal , phi( Ordinal) -> Ordinal } :

ex a st a() in a & phi(a) = a

      provided

       A1: for a, b st a in b holds phi(a) in phi(b)

       and

       A2: for a st a is non empty limit_ordinal holds for phi be Ordinal-Sequence st ( dom phi) = a & for b st b in a holds (phi . b) = phi(b) holds phi(a) is_limes_of phi;

      assume

       A3: not thesis;

      deffunc F( Ordinal, Ordinal) = phi($2);

      deffunc G( Ordinal, Sequence) = {} ;

      consider phi be Ordinal-Sequence such that

       A4: ( dom phi) = omega and

       A5: 0 in omega implies (phi . 0 ) = ( succ a()) and

       A6: for a st ( succ a) in omega holds (phi . ( succ a)) = F(a,.) and for a st a in omega & a <> 0 & a is limit_ordinal holds (phi . a) = G(a,|) from ORDINAL2:sch 11;

       A7:

      now

        defpred P[ Ordinal] means not $1 c= phi($1);

        assume

         A8: ex a st P[a];

        consider a such that

         A9: P[a] and

         A10: for b st P[b] holds a c= b from ORDINAL1:sch 1( A8);

        phi(phi) in phi(a) by A1, A9, ORDINAL1: 16;

        then not phi(a) c= phi(phi) by ORDINAL1: 5;

        hence contradiction by A9, A10;

      end;

       A11:

      now

        let a;

        assume a() in a;

        then a c= phi(a) & a <> phi(a) by A3, A7;

        then a c< phi(a);

        hence a in phi(a) by ORDINAL1: 11;

      end;

      

       A12: for a st a in omega holds a() in (phi . a)

      proof

        let a;

        assume a in omega ;

        then

        reconsider a as Element of omega ;

        defpred N[ Nat] means a() in (phi . $1);

        

         A13: N[ 0 ] by A5, ORDINAL1: 6;

         A14:

        now

          let n be Nat;

          assume

           A15: N[n];

          ( Segm (n + 1)) = ( succ ( Segm n)) & (n + 1) in omega by NAT_1: 38;

          then (phi . (n + 1)) = phi(.) by A6;

          then (phi . n) in (phi . (n + 1)) by A15, A11;

          hence N[(n + 1)] by A15, ORDINAL1: 10;

        end;

        for n be Nat holds N[n] from NAT_1:sch 2( A13, A14);

        then N[a];

        hence thesis;

      end;

      

       A16: phi is increasing

      proof

        let a, b;

        assume

         A17: a in b & b in ( dom phi);

        then

         A18: ex c st b = (a +^ c) & c <> {} by ORDINAL3: 28;

        defpred R[ Ordinal] means (a +^ $1) in omega & $1 <> {} implies (phi . a) in (phi . (a +^ $1));

        

         A19: R[ 0 ];

        

         A20: for c st R[c] holds R[( succ c)]

        proof

          let c such that

           A21: (a +^ c) in omega & c <> {} implies (phi . a) in (phi . (a +^ c)) and

           A22: (a +^ ( succ c)) in omega & ( succ c) <> {} ;

          

           A23: (a +^ c) in ( succ (a +^ c)) & (a +^ ( succ c)) = ( succ (a +^ c)) by ORDINAL1: 6, ORDINAL2: 28;

          reconsider d = (phi . (a +^ c)) as Ordinal;

          (a +^ c) in omega by A22, A23, ORDINAL1: 10;

          then (phi . (a +^ ( succ c))) = phi(d) & d in phi(d) & (a +^ {} qua Ordinal) = a by A6, A11, A22, A23, A12, ORDINAL2: 27;

          hence thesis by A21, A22, A23, ORDINAL1: 10;

        end;

        

         A24: for b st b <> 0 & b is limit_ordinal & for c st c in b holds R[c] holds R[b]

        proof

          let b such that

           A25: b <> 0 & 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

           A26: (a +^ b) in omega & b <> {} ;

          (a +^ b) <> {} by A26, ORDINAL3: 26;

          then (a +^ b) is limit_ordinal & {} in (a +^ b) by A25, ORDINAL3: 8, ORDINAL3: 29;

          hence thesis by A26;

        end;

        for c holds R[c] from ORDINAL2:sch 1( A19, A20, A24);

        hence thesis by A4, A17, A18;

      end;

      deffunc phi( Ordinal) = phi($1);

      consider fi be Ordinal-Sequence such that

       A27: ( dom fi) = ( sup phi) & for a st a in ( sup phi) holds (fi . a) = phi(a) from ORDINAL2:sch 3;

      ( succ a()) in ( rng phi) & ( sup ( rng phi)) = ( sup phi) by A4, A5, FUNCT_1:def 3;

      then

       A28: ( sup phi) <> {} & ( sup phi) is limit_ordinal by A4, A16, ORDINAL2: 19, ORDINAL4: 16;

      then

       A29: phi(sup) is_limes_of fi by A2, A27;

      fi is increasing

      proof

        let a, b;

        assume

         A30: a in b & b in ( dom fi);

        then (fi . a) = phi(a) & (fi . b) = phi(b) by A27, ORDINAL1: 10;

        hence thesis by A1, A30;

      end;

      

      then

       A31: ( sup fi) = ( lim fi) by A27, A28, ORDINAL4: 8

      .= phi(sup) by A29, ORDINAL2:def 10;

      

       A32: ( sup fi) c= ( sup phi)

      proof

        let x be Ordinal;

        assume

         A33: x in ( sup fi);

        reconsider A = x as Ordinal;

        consider b such that

         A34: b in ( rng fi) & A c= b by A33, ORDINAL2: 21;

        consider y be object such that

         A35: y in ( dom fi) & b = (fi . y) by A34, FUNCT_1:def 3;

        reconsider y as Ordinal by A35;

        consider c such that

         A36: c in ( rng phi) & y c= c by A27, A35, ORDINAL2: 21;

        consider z be object such that

         A37: z in ( dom phi) & c = (phi . z) by A36, FUNCT_1:def 3;

        reconsider z as Ordinal by A37;

        ( succ z) in omega by A4, A37, ORDINAL1: 28;

        then

         A38: (phi . ( succ z)) = phi(c) & (phi . ( succ z)) in ( rng phi) & b = phi(y) by A4, A6, A27, A35, A37, FUNCT_1:def 3;

        y c< c iff y <> c & y c= c;

        then phi(y) in phi(c) or y = c by A1, A36, ORDINAL1: 11;

        then b c= phi(c) & phi(c) in ( sup phi) by A38, ORDINAL1:def 2, ORDINAL2: 19;

        then b in ( sup phi) by ORDINAL1: 12;

        hence thesis by A34, ORDINAL1: 12;

      end;

      (phi . 0 ) in ( rng phi) by A4, FUNCT_1:def 3;

      then a() in (phi . 0 ) & (phi . 0 ) in ( sup phi) by A12, ORDINAL2: 19;

      then a() in ( sup phi) by ORDINAL1: 10;

      hence contradiction by A11, A31, A32, ORDINAL1: 5;

    end;

    begin

    definition

      let a be Ordinal;

      :: ORDINAL5:def5

      attr a is epsilon means

      : Def5: ( exp ( omega ,a)) = a;

    end

    theorem :: ORDINAL5:33

    

     Th33: ex b st a in b & b is epsilon

    proof

      deffunc phi( Ordinal) = ( exp ( omega ,$1));

      

       A1: for a, b st a in b holds phi(a) in phi(b) by ORDINAL4: 24;

       A2:

      now

        let a such that

         A3: a is non empty limit_ordinal;

        let phi be Ordinal-Sequence such that

         A4: ( dom phi) = a & for b st b in a holds (phi . b) = phi(b);

        phi is non-decreasing

        proof

          let b, c;

          assume

           A5: b in c & c in ( dom phi);

          then (phi . b) = phi(b) & (phi . c) = phi(c) by A4, ORDINAL1: 10;

          then (phi . b) in (phi . c) by A5, ORDINAL4: 24;

          hence thesis by ORDINAL1:def 2;

        end;

        then ( Union phi) is_limes_of phi & phi(a) = ( lim phi) by A3, A4, Th6, ORDINAL2: 45;

        hence phi(a) is_limes_of phi by ORDINAL2:def 10;

      end;

      consider b such that

       A6: a in b & phi(b) = b from CriticalNumber3( A1, A2);

      take b;

      thus a in b by A6;

      thus ( exp ( omega ,b)) = b by A6;

    end;

    registration

      cluster epsilon for Ordinal;

      existence

      proof

        ex a st 0 in a & a is epsilon by Th33;

        hence thesis;

      end;

    end

    definition

      let a be Ordinal;

      :: ORDINAL5:def6

      func first_epsilon_greater_than a -> epsilon Ordinal means

      : Def6: a in it & for b be epsilon Ordinal st a in b holds it c= b;

      existence

      proof

        defpred E[ Ordinal] means a in $1 & $1 is epsilon;

        

         A1: ex c st E[c] by Th33;

        consider c such that

         A2: E[c] & for b st E[b] holds c c= b from ORDINAL1:sch 1( A1);

        reconsider c as epsilon Ordinal by A2;

        take c;

        thus thesis by A2;

      end;

      uniqueness ;

    end

    theorem :: ORDINAL5:34

    a c= b implies ( first_epsilon_greater_than a) c= ( first_epsilon_greater_than b)

    proof

      assume

       A1: a c= b;

      b in ( first_epsilon_greater_than b) by Def6;

      then a in ( first_epsilon_greater_than b) by A1, ORDINAL1: 12;

      hence thesis by Def6;

    end;

    theorem :: ORDINAL5:35

    a in b & b in ( first_epsilon_greater_than a) implies ( first_epsilon_greater_than b) = ( first_epsilon_greater_than a)

    proof

      assume

       A1: a in b & b in ( first_epsilon_greater_than a);

      now

        let c be epsilon Ordinal;

        assume b in c;

        then a in c by A1, ORDINAL1: 10;

        hence ( first_epsilon_greater_than a) c= c by Def6;

      end;

      hence ( first_epsilon_greater_than b) = ( first_epsilon_greater_than a) by A1, Def6;

    end;

    theorem :: ORDINAL5:36

    

     Th36: ( first_epsilon_greater_than 0 ) = ( omega |^|^ omega )

    proof

      deffunc phi( Ordinal) = ( exp ( omega ,$1));

      

       A1: for a, b st a in b holds phi(a) in phi(b) by ORDINAL4: 24;

       A2:

      now

        let a such that

         A3: a is non empty limit_ordinal;

        let phi be Ordinal-Sequence such that

         A4: ( dom phi) = a & for b st b in a holds (phi . b) = phi(b);

        phi is non-decreasing

        proof

          let b, c;

          assume

           A5: b in c & c in ( dom phi);

          then (phi . b) = phi(b) & (phi . c) = phi(c) by A4, ORDINAL1: 10;

          then (phi . b) in (phi . c) by A5, ORDINAL4: 24;

          hence thesis by ORDINAL1:def 2;

        end;

        then ( Union phi) is_limes_of phi & phi(a) = ( lim phi) by A3, A4, Th6, ORDINAL2: 45;

        hence phi(a) is_limes_of phi by ORDINAL2:def 10;

      end;

      deffunc F( Ordinal, Ordinal) = phi($2);

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

      consider f be Ordinal-Sequence such that

       A6: ( dom f) = omega and

       A7: 0 in omega implies (f . 0 ) = 1 and

       A8: for a st ( succ a) in omega holds (f . ( succ a)) = F(a,.) and for a st a in omega & a <> 0 & a is limit_ordinal holds (f . a) = G(a,|) from ORDINAL2:sch 11;

      

       A9: ( dom f) = omega & (f . 0 ) = 1 by A6, A7;

      

       A10: for a st a in omega holds (f . ( succ a)) = phi(.) by A8, ORDINAL1: 28;

      

       A11: 1 c= ( Union f) & phi(Union) = ( Union f) & for b st 1 c= b & phi(b) = b holds ( Union f) c= b from CriticalNumber2( A1, A2, A9, A10);

      ( Union f) is epsilon by A11;

      then

      reconsider e = ( Union f) as epsilon Ordinal;

      defpred I[ Nat] means (f . $1) = ( omega |^|^ $1);

      

       A12: I[ 0 ] by A7, Th13;

      

       A13: for n st I[n] holds I[(n + 1)]

      proof

        let n such that

         A14: I[n];

        

         A15: ( Segm (n + 1)) = ( succ ( Segm n)) & n in omega by NAT_1: 38, ORDINAL1:def 12;

        

        hence (f . (n + 1)) = phi(.) by A10

        .= ( omega |^|^ (n + 1)) by A14, A15, Th14;

      end;

      

       A16: for n holds I[n] from NAT_1:sch 2( A12, A13);

      then for c st c in omega holds (f . c) = ( omega |^|^ c);

      then

       A17: ( omega |^|^ omega ) = ( lim f) by A6, Th15;

      f is non-decreasing

      proof

        let a, b;

        assume

         A18: a in b & b in ( dom f);

        then

        reconsider n = a, m = b as Element of omega by A6, ORDINAL1: 10;

        a c= b by A18, ORDINAL1:def 2;

        then ( omega |^|^ a) c= ( omega |^|^ b) by Th21;

        then (f . n) c= ( omega |^|^ m) by A16;

        hence thesis by A16;

      end;

      then e is_limes_of f by A6, Th6;

      then

       A19: ( omega |^|^ omega ) = e by A17, ORDINAL2:def 10;

      

       A20: ( succ 0 ) = 1;

      then

       A21: 0 in 1 by ORDINAL1: 6;

      now

        let b be epsilon Ordinal;

        assume 0 in b;

        then 1 c= b & phi(b) = b by A20, Def5, ORDINAL1: 21;

        hence e c= b by A11;

      end;

      hence thesis by A19, A21, Def6, A11;

    end;

    theorem :: ORDINAL5:37

    

     Th37: for e be epsilon Ordinal holds omega in e

    proof

      let e be epsilon Ordinal;

      

       A1: ( exp ( omega ,e)) = e by Def5;

      

       A2: ( exp ( omega , 0 )) = 1 & ( exp ( omega ,1)) = omega & 1 in omega by ORDINAL2: 43, ORDINAL2: 46;

      then

       A3: e <> 0 & e <> 1 & ( succ 0 ) = 1 & ( succ 1) = 2 by Def5;

      then 0 in e by ORDINAL3: 8;

      then 1 c= e by A3, ORDINAL1: 21;

      then 1 c< e by A3;

      then 1 in e by ORDINAL1: 11;

      hence thesis by A1, A2, ORDINAL4: 24;

    end;

    registration

      cluster epsilon -> non empty limit_ordinal for Ordinal;

      coherence

      proof

        let e be Ordinal such that

         A1: e is epsilon;

        ( exp ( omega , 0 )) = 1 by ORDINAL2: 43;

        hence e is non empty by A1;

        then 0 in e & ( exp ( omega ,e)) = e by A1, ORDINAL3: 8;

        hence thesis by Th9;

      end;

    end

    theorem :: ORDINAL5:38

    

     Th38: for e be epsilon Ordinal holds ( exp ( omega ,( exp (e, omega )))) = ( exp (e,( exp (e, omega ))))

    proof

      let e be epsilon Ordinal;

      

      thus ( exp ( omega ,( exp (e, omega )))) = ( exp ( omega ,( exp (e,(1 +^ omega ))))) by CARD_2: 74

      .= ( exp ( omega ,(( exp (e, omega )) *^ ( exp (e,1))))) by ORDINAL4: 30

      .= ( exp ( omega ,(( exp (e, omega )) *^ e))) by ORDINAL2: 46

      .= ( exp (( exp ( omega ,e)),( exp (e, omega )))) by ORDINAL4: 31

      .= ( exp (e,( exp (e, omega )))) by Def5;

    end;

    theorem :: ORDINAL5:39

    

     Th39: for e be epsilon Ordinal st 0 in n holds (e |^|^ (n + 2)) = ( exp ( omega ,(e |^|^ (n + 1))))

    proof

      let e be epsilon Ordinal such that

       A1: 0 in n;

       0 in e by ORDINAL3: 8;

      then omega in e & e c= (e |^|^ n) by A1, Th23, Th37;

      then

       A2: omega c= (e |^|^ n) by ORDINAL1:def 2;

      

      thus (e |^|^ (n + 2)) = (e |^|^ ( Segm ((n + 1) + 1)))

      .= (e |^|^ ( succ ( Segm (n + 1)))) by NAT_1: 38

      .= ( exp (e,(e |^|^ (n + 1)))) by Th14

      .= ( exp (( exp ( omega ,e)),(e |^|^ (n + 1)))) by Def5

      .= ( exp ( omega ,((e |^|^ ( Segm (n + 1))) *^ e))) by ORDINAL4: 31

      .= ( exp ( omega ,((e |^|^ ( succ ( Segm n))) *^ e))) by NAT_1: 38

      .= ( exp ( omega ,(( exp (e,(e |^|^ n))) *^ e))) by Th14

      .= ( exp ( omega ,(( exp (e,(e |^|^ n))) *^ ( exp (e,1))))) by ORDINAL2: 46

      .= ( exp ( omega ,( exp (e,(1 +^ (e |^|^ n)))))) by ORDINAL4: 30

      .= ( exp ( omega ,( exp (e,(e |^|^ n))))) by A2, CARD_2: 74

      .= ( exp ( omega ,(e |^|^ ( succ ( Segm n))))) by Th14

      .= ( exp ( omega ,(e |^|^ ( Segm (n + 1))))) by NAT_1: 38

      .= ( exp ( omega ,(e |^|^ (n + 1))));

    end;

    theorem :: ORDINAL5:40

    

     Th40: for e be epsilon Ordinal holds ( first_epsilon_greater_than e) = (e |^|^ omega )

    proof

      let e be epsilon Ordinal;

      deffunc phi( Ordinal) = ( exp ( omega ,$1));

      

       A1: for a, b st a in b holds phi(a) in phi(b) by ORDINAL4: 24;

       A2:

      now

        let a such that

         A3: a is non empty limit_ordinal;

        let phi be Ordinal-Sequence such that

         A4: ( dom phi) = a & for b st b in a holds (phi . b) = phi(b);

        phi is non-decreasing

        proof

          let b, c;

          assume

           A5: b in c & c in ( dom phi);

          then (phi . b) = phi(b) & (phi . c) = phi(c) by A4, ORDINAL1: 10;

          then (phi . b) in (phi . c) by A5, ORDINAL4: 24;

          hence thesis by ORDINAL1:def 2;

        end;

        then ( Union phi) is_limes_of phi & phi(a) = ( lim phi) by A3, A4, Th6, ORDINAL2: 45;

        hence phi(a) is_limes_of phi by ORDINAL2:def 10;

      end;

      deffunc F( Ordinal, Ordinal) = phi($2);

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

      consider f be Ordinal-Sequence such that

       A6: ( dom f) = omega and

       A7: 0 in omega implies (f . 0 ) = ( succ e) and

       A8: for a st ( succ a) in omega holds (f . ( succ a)) = F(a,.) and for a st a in omega & a <> 0 & a is limit_ordinal holds (f . a) = G(a,|) from ORDINAL2:sch 11;

      

       A9: ( dom f) = omega & (f . 0 ) = ( succ e) by A6, A7;

      

       A10: for a st a in omega holds (f . ( succ a)) = phi(.) by A8, ORDINAL1: 28;

      

       A11: ( succ e) c= ( Union f) & phi(Union) = ( Union f) & for b st ( succ e) c= b & phi(b) = b holds ( Union f) c= b from CriticalNumber2( A1, A2, A9, A10);

      ( Union f) is epsilon by A11;

      then

      reconsider e9 = ( Union f) as epsilon Ordinal;

       A12:

      now

        e in ( succ e) by ORDINAL1: 6;

        hence e in e9 by A11;

        let b be epsilon Ordinal;

        assume e in b;

        then ( succ e) c= b & phi(b) = b by Def5, ORDINAL1: 21;

        hence e9 c= b by A11;

      end;

      

       A13: ( succ 0 ) = 1 & ( succ 1) = 2 & ( succ 2) = 3;

      

      then

       A14: (f . 1) = phi(succ) by A7, A8

      .= ( omega *^ phi(e)) by ORDINAL2: 44

      .= ( omega *^ e) by Def5;

      

      then

       A15: (f . 2) = phi(*^) by A13, A8

      .= ( exp ( phi(e), omega )) by ORDINAL4: 31

      .= ( exp (e, omega )) by Def5;

      

      then

       A16: (f . 3) = phi(exp) by A13, A8

      .= ( exp (e,( exp (e, omega )))) by Th38;

      

       A17: (e |^|^ 0 ) = 1 & (e |^|^ 1) = e & (e |^|^ 2) = ( exp (e,e)) by Th13, Th16, Th18;

       omega in e & 1 in omega by Th37;

      then

       A18: 1 in e by ORDINAL1: 10;

      then ( exp (e,1)) in ( exp (e,e)) & ( exp (e,1)) in ( exp (e, omega )) by ORDINAL4: 24;

      then

       A19: e in ( exp (e,e)) & e in ( exp (e, omega )) by ORDINAL2: 46;

      defpred I[ Nat] means (e |^|^ $1) in (f . ($1 + 1)) & (f . $1) in (e |^|^ ($1 + 2));

      e in ( exp (e,e)) & ( exp (e,e)) is limit_ordinal by A17, A18, Th24, Th9, ORDINAL3: 8;

      then

       A20: I[ 0 ] by A7, A14, A17, ORDINAL1: 28, ORDINAL3: 32;

      

       A21: for n st I[n] holds I[(n + 1)]

      proof

        let n such that

         A22: I[n];

        

         A23: ( Segm (n + 1)) = ( succ ( Segm n)) & ( Segm ((n + 1) + 1)) = ( succ ( Segm (n + 1))) & n in omega & (n + 1) in omega by NAT_1: 38, ORDINAL1:def 12;

        then

         A24: (f . (n + 1)) = phi(.) & (f . ((n + 1) + 1)) = phi(.) by A10;

        thus (e |^|^ (n + 1)) in (f . ((n + 1) + 1))

        proof

          per cases by NAT_1: 23;

            suppose n = 0 ;

            hence thesis by A15, Th16, A19;

          end;

            suppose n = 1;

            hence thesis by A16, A17, A18, A19, ORDINAL4: 24;

          end;

            suppose n >= 2;

            then

            consider k be Nat such that

             A25: n = (2 + k) by NAT_1: 10;

             0 in ( Segm (k + 1)) & (k + 2) = ((k + 1) + 1) by NAT_1: 44;

            then phi(|^|^) = (e |^|^ ((k + 1) + 2)) by Th39;

            hence thesis by A24, A25, A22, ORDINAL4: 24;

          end;

        end;

         0 in ( Segm (n + 1)) & (n + 2) = ((n + 1) + 1) by NAT_1: 44;

        then phi(|^|^) = (e |^|^ ((n + 1) + 2)) by Th39;

        then phi(.) in (e |^|^ ((n + 1) + 2)) by A22, ORDINAL4: 24;

        hence (f . (n + 1)) in (e |^|^ ((n + 1) + 2)) by A23, A10;

      end;

      

       A26: for n holds I[n] from NAT_1:sch 2( A20, A21);

      deffunc G( Ordinal) = (e |^|^ $1);

      consider g be Ordinal-Sequence such that

       A27: ( dom g) = omega & for a st a in omega holds (g . a) = G(a) from ORDINAL2:sch 3;

      

       A28: (e |^|^ omega ) = ( lim g) by A27, Th15;

      1 in omega & omega in e by Th37;

      then 1 in e by ORDINAL1: 10;

      then g is increasing Ordinal-Sequence by A27, Th25;

      then ( Union g) is_limes_of g by A27, Th6;

      then

       A29: (e |^|^ omega ) = ( Union g) by A28, ORDINAL2:def 10;

      e9 = ( Union g)

      proof

        thus e9 c= ( Union g)

        proof

          let x be Ordinal;

          assume x in e9;

          then

          consider a be object such that

           A30: a in ( dom f) & x in (f . a) by CARD_5: 2;

          reconsider a as Element of omega by A6, A30;

          (f . a) in (e |^|^ (a + 2)) & (g . (a + 2)) = G(+) by A26, A27;

          then (f . a) in ( Union g) by A27, CARD_5: 2;

          hence thesis by A30, ORDINAL1: 10;

        end;

        let x be Ordinal;

        assume x in ( Union g);

        then

        consider a be object such that

         A31: a in ( dom g) & x in (g . a) by CARD_5: 2;

        reconsider a as Element of omega by A27, A31;

        (a + 1) in omega & (e |^|^ a) in (f . (a + 1)) & (g . a) = G(a) by A26, A27;

        then (g . a) in ( Union f) by A6, CARD_5: 2;

        hence thesis by A31, ORDINAL1: 10;

      end;

      hence thesis by A12, A29, Def6;

    end;

    definition

      let a be Ordinal;

      :: ORDINAL5:def7

      func epsilon_ a -> Ordinal means

      : Def7: ex phi be Ordinal-Sequence st it = ( last phi) & ( dom phi) = ( succ a) & (phi . {} ) = ( omega |^|^ omega ) & (for b be Ordinal st ( succ b) in ( succ a) holds (phi . ( succ b)) = ((phi . b) |^|^ omega )) & for c be Ordinal st c in ( succ a) & c <> {} & c is limit_ordinal holds (phi . c) = ( lim (phi | c));

      correctness

      proof

        deffunc C( Ordinal, Ordinal) = ($2 |^|^ omega );

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

        (ex F be Ordinal, fi be Ordinal-Sequence st F = ( last fi) & ( dom fi) = ( succ a) & (fi . 0 ) = ( omega |^|^ omega ) & (for c be Ordinal st ( succ c) in ( succ a) holds (fi . ( succ c)) = C(c,.)) & for c be Ordinal st c in ( succ a) & c <> 0 & c is limit_ordinal holds (fi . c) = D(c,|)) & for A1,A2 be Ordinal st (ex fi be Ordinal-Sequence st A1 = ( last fi) & ( dom fi) = ( succ a) & (fi . 0 ) = ( omega |^|^ omega ) & (for C be Ordinal st ( succ C) in ( succ a) holds (fi . ( succ C)) = C(C,.)) & for C be Ordinal st C in ( succ a) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|)) & (ex fi be Ordinal-Sequence st A2 = ( last fi) & ( dom fi) = ( succ a) & (fi . 0 ) = ( omega |^|^ omega ) & (for C be Ordinal st ( succ C) in ( succ a) holds (fi . ( succ C)) = C(C,.)) & for C be Ordinal st C in ( succ a) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|)) holds A1 = A2 from ORDINAL2:sch 13;

        hence thesis;

      end;

    end

    theorem :: ORDINAL5:41

    

     Th41: ( epsilon_ 0 ) = ( omega |^|^ omega )

    proof

      deffunc F( Ordinal) = ( epsilon_ $1);

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

      deffunc C( Ordinal, Ordinal) = ($2 |^|^ omega );

      

       A1: for b, c holds c = F(b) iff ex fi be Ordinal-Sequence st c = ( last fi) & ( dom fi) = ( succ b) & (fi . 0 ) = ( omega |^|^ omega ) & (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 Def7;

      thus F(0) = ( omega |^|^ omega ) from ORDINAL2:sch 14( A1);

    end;

    theorem :: ORDINAL5:42

    

     Th42: ( epsilon_ ( succ a)) = (( epsilon_ a) |^|^ omega )

    proof

      deffunc F( Ordinal) = ( epsilon_ $1);

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

      deffunc C( Ordinal, Ordinal) = ($2 |^|^ omega );

      

       A1: for b, c holds c = F(b) iff ex fi be Ordinal-Sequence st c = ( last fi) & ( dom fi) = ( succ b) & (fi . 0 ) = ( omega |^|^ omega ) & (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 Def7;

      for b holds F(succ) = C(b,F) from ORDINAL2:sch 15( A1);

      hence thesis;

    end;

    theorem :: ORDINAL5:43

    

     Th43: b <> 0 & b is limit_ordinal implies for phi be Ordinal-Sequence st ( dom phi) = b & for c st c in b holds (phi . c) = ( epsilon_ c) holds ( epsilon_ b) = ( lim phi)

    proof

      assume

       A1: b <> 0 & b is limit_ordinal;

      deffunc F( Ordinal) = ( epsilon_ $1);

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

      deffunc C( Ordinal, Ordinal) = ($2 |^|^ omega );

      let fi be Ordinal-Sequence 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 be Ordinal-Sequence st c = ( last fi) & ( dom fi) = ( succ b) & (fi . 0 ) = ( omega |^|^ omega ) & (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 Def7;

      thus F(b) = D(b,fi) from ORDINAL2:sch 16( A4, A1, A2, A3);

    end;

    theorem :: ORDINAL5:44

    

     Th44: a in b implies ( epsilon_ a) in ( epsilon_ b)

    proof

      defpred P[ Ordinal] means 1 in ( epsilon_ $1) & for a, b st a in b & b c= $1 holds ( epsilon_ a) in ( epsilon_ b);

       omega in ( epsilon_ 0 ) by Th26, Th41;

      then

       A1: P[ 0 ] by ORDINAL1: 10;

      

       A2: P[c] implies P[( succ c)]

      proof

        assume

         A3: P[c];

        

         A4: ( epsilon_ ( succ c)) = (( epsilon_ c) |^|^ omega ) by Th42;

        then

         A5: ( epsilon_ c) in ( epsilon_ ( succ c)) by A3, Th26;

        hence 1 in ( epsilon_ ( succ c)) by A3, ORDINAL1: 10;

        let a, b;

        assume

         A6: a in b & b c= ( succ c);

        then a c= c by ORDINAL1: 22;

        then

         A7: b = ( succ c) & (a = c or a c< c) or b c< ( succ c) by A6;

        per cases by A7, ORDINAL1: 11;

          suppose b in ( succ c);

          then b c= c by ORDINAL1: 22;

          hence thesis by A3, A6;

        end;

          suppose

           A8: b = ( succ c) & a in c;

          then ( epsilon_ a) in ( epsilon_ c) by A3;

          hence thesis by A5, A8, ORDINAL1: 10;

        end;

          suppose b = ( succ c) & a = c;

          hence thesis by A3, A4, Th26;

        end;

      end;

      

       A9: c <> 0 & c is limit_ordinal & (for b st b in c holds P[b]) implies P[c]

      proof

        assume that

         A10: c <> 0 & c is limit_ordinal and

         A11: for b st b in c holds P[b];

        deffunc F( Ordinal) = ( epsilon_ $1);

        consider f such that

         A12: ( dom f) = c & for b st b in c holds (f . b) = F(b) from ORDINAL2:sch 3;

        f is increasing

        proof

          let a, b;

          assume

           A13: a in b & b in ( dom f);

          then a in c by A12, ORDINAL1: 10;

          then (f . a) = F(a) & (f . b) = F(b) & P[b] by A11, A12, A13;

          hence thesis by A13;

        end;

        then ( Union f) is_limes_of f by A10, A12, Th6;

        

        then

         A14: ( Union f) = ( lim f) by ORDINAL2:def 10

        .= ( epsilon_ c) by A10, A12, Th43;

        

         A15: 0 in c by A10, ORDINAL3: 8;

        then 1 in ( epsilon_ 0 ) & (f . 0 ) = F(0) by A11, A12;

        hence 1 in ( epsilon_ c) by A12, A14, A15, CARD_5: 2;

        let a, b;

        assume

         A16: a in b & b c= c;

        then

         A17: b = c or b c< c;

        per cases by A17, ORDINAL1: 11;

          suppose b in c;

          hence ( epsilon_ a) in ( epsilon_ b) by A11, A16;

        end;

          suppose

           A18: b = c;

          ( succ a) in c & a in ( succ a) by A10, A16, ORDINAL1: 6, ORDINAL1: 28;

          then

           A19: F(a) in F(succ) & F(succ) = (f . ( succ a)) & (f . ( succ a)) in ( rng f) by A11, A12, FUNCT_1:def 3;

          then (f . ( succ a)) c= ( Union f) by ZFMISC_1: 74;

          hence thesis by A14, A18, A19;

        end;

      end;

       P[c] from ORDINAL2:sch 1( A1, A2, A9);

      hence thesis;

    end;

    theorem :: ORDINAL5:45

    

     Th45: for phi be Ordinal-Sequence st for c st c in ( dom phi) holds (phi . c) = ( epsilon_ c) holds phi is increasing

    proof

      let f;

      assume

       A1: for c st c in ( dom f) holds (f . c) = ( epsilon_ c);

      let a, b;

      assume

       A2: a in b & b in ( dom f);

      then (f . a) = ( epsilon_ a) & (f . b) = ( epsilon_ b) by A1, ORDINAL1: 10;

      hence thesis by A2, Th44;

    end;

    theorem :: ORDINAL5:46

    

     Th46: b <> {} & b is limit_ordinal implies for phi be Ordinal-Sequence st ( dom phi) = b & for c st c in b holds (phi . c) = ( epsilon_ c) holds ( epsilon_ b) = ( Union phi)

    proof

      assume

       A1: b <> {} & b is limit_ordinal;

      let f;

      assume

       A2: ( dom f) = b & for c st c in b holds (f . c) = ( epsilon_ c);

      then f is increasing Ordinal-Sequence by Th45;

      then ( Union f) is_limes_of f by A1, A2, Th6;

      then ( Union f) = ( lim f) by ORDINAL2:def 10;

      hence thesis by A1, A2, Th43;

    end;

    theorem :: ORDINAL5:47

    

     Th47: b is non empty limit_ordinal implies (x in ( epsilon_ b) iff ex c st c in b & x in ( epsilon_ c))

    proof

      assume

       A1: b is non empty limit_ordinal;

      deffunc F( Ordinal) = ( epsilon_ $1);

      consider f such that

       A2: ( dom f) = b & for c st c in b holds (f . c) = F(c) from ORDINAL2:sch 3;

      

       A3: ( Union f) = ( epsilon_ b) by A1, A2, Th46;

      hereby

        assume x in ( epsilon_ b);

        then

        consider c be object such that

         A4: c in ( dom f) & x in (f . c) by A3, CARD_5: 2;

        reconsider c as Ordinal by A4;

        take c;

        thus c in b by A2, A4;

        thus x in ( epsilon_ c) by A2, A4;

      end;

      given c such that

       A5: c in b & x in ( epsilon_ c);

      (f . c) = F(c) by A2, A5;

      hence x in ( epsilon_ b) by A2, A3, A5, CARD_5: 2;

    end;

    theorem :: ORDINAL5:48

    

     Th48: a c= ( epsilon_ a)

    proof

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

      

       A1: P[ 0 ];

      

       A2: P[b] implies P[( succ b)]

      proof

        assume

         A3: P[b];

        ( epsilon_ b) in ( epsilon_ ( succ b)) by Th44, ORDINAL1: 6;

        then b in ( epsilon_ ( succ b)) by A3, ORDINAL1: 12;

        hence thesis by ORDINAL1: 21;

      end;

      

       A4: c <> 0 & c is limit_ordinal & (for b st b in c holds P[b]) implies P[c]

      proof

        assume that c <> 0 & c is limit_ordinal and

         A5: for b st b in c holds P[b];

        let x be Ordinal;

        assume

         A6: x in c;

        reconsider a = x as Ordinal;

         P[a] & ( epsilon_ a) in ( epsilon_ c) by A5, A6, Th44;

        hence thesis by ORDINAL1: 12;

      end;

       P[b] from ORDINAL2:sch 1( A1, A2, A4);

      hence thesis;

    end;

    theorem :: ORDINAL5:49

    

     Th49: for X be non empty set st for x st x in X holds x is epsilon Ordinal & ex e be epsilon Ordinal st x in e & e in X holds ( union X) is epsilon Ordinal

    proof

      let X be non empty set;

      assume

       A1: for x st x in X holds x is epsilon Ordinal & ex e be epsilon Ordinal st x in e & e in X;

      then for x st x in X holds x is Ordinal;

      then

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

      now

        let b;

        assume b in a;

        then

        consider x be set such that

         A2: b in x & x in X by TARSKI:def 4;

        reconsider x as epsilon Ordinal by A2, A1;

        ( succ b) in x by A2, ORDINAL1: 28;

        hence ( succ b) in a by A2, TARSKI:def 4;

      end;

      then

       A3: a is limit_ordinal by ORDINAL1: 28;

      set z = the Element of X;

      ex e be epsilon Ordinal st z in e & e in X by A1;

      then

       A4: a <> {} by TARSKI:def 4;

      a is epsilon

      proof

        thus ( exp ( omega ,a)) c= a

        proof

          let x be Ordinal;

          assume x in ( exp ( omega ,a));

          then

          consider b such that

           A5: b in a & x in ( exp ( omega ,b)) by A3, A4, Th11;

          consider y be set such that

           A6: b in y & y in X by A5, TARSKI:def 4;

          reconsider y as epsilon Ordinal by A1, A6;

          ( exp ( omega ,b)) in ( exp ( omega ,y)) by A6, ORDINAL4: 24;

          then ( exp ( omega ,b)) in y by Def5;

          then x in y by A5, ORDINAL1: 10;

          hence thesis by A6, TARSKI:def 4;

        end;

        thus thesis by ORDINAL4: 32;

      end;

      hence thesis;

    end;

    theorem :: ORDINAL5:50

    

     Th50: for X be non empty set st (for x st x in X holds x is epsilon Ordinal) & for a st a in X holds ( first_epsilon_greater_than a) in X holds ( union X) is epsilon Ordinal

    proof

      let X be non empty set such that

       A1: for x st x in X holds x is epsilon Ordinal and

       A2: for a st a in X holds ( first_epsilon_greater_than a) in X;

      now

        let x;

        assume

         A3: x in X;

        hence x is epsilon Ordinal by A1;

        reconsider a = x as Ordinal by A1, A3;

        take e = ( first_epsilon_greater_than a);

        thus x in e & e in X by A2, A3, Def6;

      end;

      hence ( union X) is epsilon Ordinal by Th49;

    end;

    registration

      let a;

      cluster ( epsilon_ a) -> epsilon;

      coherence

      proof

        deffunc phi( Ordinal) = ( epsilon_ $1);

        defpred P[ Ordinal] means phi($1) is epsilon;

        

         A1: P[ 0 ] by Th36, Th41;

        

         A2: P[b] implies P[( succ b)]

        proof

          assume P[b];

          

          then ( first_epsilon_greater_than ( epsilon_ b)) = (( epsilon_ b) |^|^ omega ) by Th40

          .= ( epsilon_ ( succ b)) by Th42;

          hence thesis;

        end;

        

         A3: b <> 0 & b is limit_ordinal & (for c st c in b holds P[c]) implies P[b]

        proof

          assume that

           A4: b <> 0 & b is limit_ordinal and

           A5: for c st c in b holds P[c];

          consider f such that

           A6: ( dom f) = b & for c st c in b holds (f . c) = phi(c) from ORDINAL2:sch 3;

          

           A7: phi(b) = ( Union f) by A4, A6, Th46;

          set X = ( rng f);

           0 in b by A4, ORDINAL3: 8;

          then (f . 0 ) in ( rng f) by A6, FUNCT_1:def 3;

          then

          reconsider X as non empty set;

           A8:

          now

            let x;

            assume x in X;

            then

            consider a be object such that

             A9: a in ( dom f) & (f . a) = x by FUNCT_1:def 3;

            reconsider a as Ordinal by A9;

            x = phi(a) by A6, A9;

            hence x is epsilon Ordinal by A5, A6, A9;

          end;

          now

            let x be Ordinal;

            assume

             A10: x in X;

            then

            consider a be object such that

             A11: a in ( dom f) & (f . a) = x by FUNCT_1:def 3;

            reconsider a as Ordinal by A11;

            

             A12: ( succ a) in b by A4, A6, A11, ORDINAL1: 28;

            reconsider e = x as epsilon Ordinal by A8, A10;

            e = phi(a) by A6, A11;

            

            then ( first_epsilon_greater_than e) = ( phi(a) |^|^ omega ) by Th40

            .= phi(succ) by Th42

            .= (f . ( succ a)) by A6, A12;

            hence ( first_epsilon_greater_than x) in X by A6, A12, FUNCT_1:def 3;

          end;

          hence P[b] by A7, A8, Th50;

        end;

        for a holds P[a] from ORDINAL2:sch 1( A1, A2, A3);

        hence thesis;

      end;

    end

    ::$Notion-Name

    theorem :: ORDINAL5:51

    a is epsilon implies ex b st a = ( epsilon_ b)

    proof

      defpred N[ set] means ex b st $1 = ( epsilon_ b);

      defpred Q[ Ordinal] means for e be epsilon Ordinal st e in ( epsilon_ $1) holds N[e];

      

       A1: Q[ 0 ]

      proof

        let e be epsilon Ordinal;

         0 in e by ORDINAL3: 8;

        then ( first_epsilon_greater_than 0 ) c= e by Def6;

        then e in ( epsilon_ 0 ) implies e in e by Th36, Th41;

        hence thesis;

      end;

      

       A2: Q[c] implies Q[( succ c)]

      proof

        assume

         A3: Q[c];

        let e be epsilon Ordinal such that

         A4: e in ( epsilon_ ( succ c));

        

         A5: ( epsilon_ ( succ c)) = (( epsilon_ c) |^|^ omega ) by Th42

        .= ( first_epsilon_greater_than ( epsilon_ c)) by Th40;

        per cases by ORDINAL1: 14;

          suppose e in ( epsilon_ c);

          hence N[e] by A3;

        end;

          suppose e = ( epsilon_ c);

          hence N[e];

        end;

          suppose ( epsilon_ c) in e;

          then ( epsilon_ ( succ c)) c= e by A5, Def6;

          then e in e by A4;

          hence N[e];

        end;

      end;

      

       A6: b <> 0 & b is limit_ordinal & (for c st c in b holds Q[c]) implies Q[b]

      proof

        assume that

         A7: b <> 0 & b is limit_ordinal and

         A8: for c st c in b holds Q[c];

        let e be epsilon Ordinal;

        assume e in ( epsilon_ b);

        then ex c st c in b & e in ( epsilon_ c) by A7, Th47;

        hence N[e] by A8;

      end;

      

       A9: Q[b] from ORDINAL2:sch 1( A1, A2, A6);

      a c= ( epsilon_ a) & ( epsilon_ a) in ( epsilon_ ( succ a)) by Th44, Th48, ORDINAL1: 6;

      hence thesis by A9, ORDINAL1: 12;

    end;

    begin

    definition

      let A be finite Ordinal-Sequence;

      :: ORDINAL5:def8

      func Sum^ A -> Ordinal means

      : Def8: ex f be Ordinal-Sequence st it = ( last f) & ( dom f) = ( succ ( dom A)) & (f . 0 ) = 0 & for n be Nat st n in ( dom A) holds (f . (n + 1)) = ((f . n) +^ (A . n));

      correctness

      proof

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

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

        set b = ( dom A);

        

         A1: (ex F be Ordinal, fi be Ordinal-Sequence st F = ( last fi) & ( dom fi) = ( succ b) & (fi . 0 ) = 0 & (for c be Ordinal st ( succ c) in ( succ b) holds (fi . ( succ c)) = C(c,.)) & for c be Ordinal st c in ( succ b) & c <> 0 & c is limit_ordinal holds (fi . c) = D(c,|)) & for A1,A2 be Ordinal st (ex fi be Ordinal-Sequence st A1 = ( last fi) & ( dom fi) = ( succ b) & (fi . 0 ) = 0 & (for C be Ordinal st ( succ C) in ( succ b) holds (fi . ( succ C)) = C(C,.)) & for C be Ordinal st C in ( succ b) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|)) & (ex fi be Ordinal-Sequence st A2 = ( last fi) & ( dom fi) = ( succ b) & (fi . 0 ) = 0 & (for C be Ordinal st ( succ C) in ( succ b) holds (fi . ( succ C)) = C(C,.)) & for C be Ordinal st C in ( succ b) & C <> 0 & C is limit_ordinal holds (fi . C) = D(C,|)) holds A1 = A2 from ORDINAL2:sch 13;

        then

        consider a, f such that

         A2: a = ( last f) & ( dom f) = ( succ b) & (f . 0 ) = 0 & (for c be Ordinal st ( succ c) in ( succ b) holds (f . ( succ c)) = C(c,.)) & for c be Ordinal st c in ( succ b) & c <> {} & c is limit_ordinal holds (f . c) = D(c,|);

        hereby

          take a, f;

          thus a = ( last f) & ( dom f) = ( succ b) & (f . 0 ) = 0 by A2;

          let n;

          assume n in ( dom A);

          then ( succ n) c= ( dom A) by ORDINAL1: 21;

          then ( succ n) in ( succ b) & ( Segm (n + 1)) = ( succ ( Segm n)) by NAT_1: 38, ORDINAL1: 22;

          hence (f . (n + 1)) = ((f . n) +^ (A . n)) by A2;

        end;

        let a1,a2 be Ordinal;

        given f1 be Ordinal-Sequence such that

         A3: a1 = ( last f1) & ( dom f1) = ( succ ( dom A)) & (f1 . 0 ) = 0 & for n be Nat st n in ( dom A) holds (f1 . (n + 1)) = ((f1 . n) +^ (A . n));

        given f2 be Ordinal-Sequence such that

         A4: a2 = ( last f2) & ( dom f2) = ( succ ( dom A)) & (f2 . 0 ) = 0 & for n be Nat st n in ( dom A) holds (f2 . (n + 1)) = ((f2 . n) +^ (A . n));

        reconsider b as finite Ordinal;

        

         A5: for c be Ordinal st ( succ c) in ( succ b) holds (f1 . ( succ c)) = C(c,.)

        proof

          let c;

          assume ( succ c) in ( succ b);

          then

           A6: c in b by ORDINAL3: 3;

          then

          reconsider n = c as Element of omega ;

          

           A7: ( Segm (n + 1)) = ( succ ( Segm n)) by NAT_1: 38;

          (f1 . (n + 1)) = C(n,.) by A3, A6;

          hence thesis by A7;

        end;

        

         A8: for c be Ordinal st c in ( succ b) & c <> {} & c is limit_ordinal holds (f1 . c) = D(c,|)

        proof

          

           A9: ( succ b) in omega by ORDINAL1:def 12;

          let c be Ordinal;

          assume

           A10: c in ( succ b) & c <> {} & c is limit_ordinal;

          then 0 in c by ORDINAL3: 8;

          then c in omega & omega c= c by A10, ORDINAL1: 10, ORDINAL1:def 11, A9;

          hence (f1 . c) = D(c,|);

        end;

        

         A11: for c be Ordinal st ( succ c) in ( succ b) holds (f2 . ( succ c)) = C(c,.)

        proof

          let c;

          assume ( succ c) in ( succ b);

          then

           A12: c in b by ORDINAL3: 3;

          then

          reconsider n = c as Element of omega ;

          

           A13: ( Segm (n + 1)) = ( succ ( Segm n)) by NAT_1: 38;

          (f2 . (n + 1)) = C(n,.) by A4, A12;

          hence thesis by A13;

        end;

        for c be Ordinal st c in ( succ b) & c <> {} & c is limit_ordinal holds (f2 . c) = D(c,|)

        proof

          let c be Ordinal;

          

           A14: ( succ b) in omega by ORDINAL1:def 12;

          assume

           A15: c in ( succ b) & c <> {} & c is limit_ordinal;

          then 0 in c by ORDINAL3: 8;

          then c in omega & omega c= c by A15, ORDINAL1: 10, ORDINAL1:def 11, A14;

          hence thesis;

        end;

        hence thesis by A1, A3, A4, A5, A8, A11;

      end;

    end

    theorem :: ORDINAL5:52

    

     Th52: ( Sum^ {} ) = 0

    proof

      reconsider A = {} as finite Ordinal-Sequence;

      consider f be Ordinal-Sequence such that

       A1: ( Sum^ A) = ( last f) and

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

       A3: (f . 0 ) = 0 and for n be Nat st n in ( dom A) holds (f . (n + 1)) = ((f . n) +^ (A . n)) by Def8;

      ( dom f) = ( succ 0 ) implies ( last f) = (f . 0 ) by ORDINAL2: 6;

      hence ( Sum^ {} ) = 0 by A1, A2, A3;

    end;

    theorem :: ORDINAL5:53

    

     Th53: ( Sum^ <%a%>) = a

    proof

      consider f be Ordinal-Sequence such that

       A1: ( Sum^ <%a%>) = ( last f) & ( dom f) = ( succ ( dom <%a%>)) & (f . 0 ) = 0 & for n be Nat st n in ( dom <%a%>) holds (f . (n + 1)) = ((f . n) +^ ( <%a%> . n)) by Def8;

      

       A2: ( dom <%a%>) = 1 & ( <%a%> . 0 ) = a by AFINSQ_1:def 4;

       0 in ( Segm 1) by NAT_1: 44;

      

      then (f . ( 0 + 1)) = ( 0 qua Ordinal +^ a) by A1, A2

      .= a by ORDINAL2: 30;

      hence thesis by A1, A2, ORDINAL2: 6;

    end;

    theorem :: ORDINAL5:54

    

     Th54: for A be finite Ordinal-Sequence holds ( Sum^ (A ^ <%a%>)) = (( Sum^ A) +^ a)

    proof

      let A be finite Ordinal-Sequence;

      consider f be Ordinal-Sequence such that

       A1: ( Sum^ (A ^ <%a%>)) = ( last f) & ( dom f) = ( succ ( dom (A ^ <%a%>))) & (f . 0 ) = 0 & for n be Nat st n in ( dom (A ^ <%a%>)) holds (f . (n + 1)) = ((f . n) +^ ((A ^ <%a%>) . n)) by Def8;

      consider g be Ordinal-Sequence such that

       A2: ( Sum^ A) = ( last g) & ( dom g) = ( succ ( dom A)) & (g . 0 ) = 0 & for n be Nat st n in ( dom A) holds (g . (n + 1)) = ((g . n) +^ (A . n)) by Def8;

      ( dom <%a%>) = 1 by AFINSQ_1:def 4;

      then

       A3: ( dom (A ^ <%a%>)) = (( dom A) +^ 1) & (( dom A) +^ 1) = ( succ ( dom A)) by ORDINAL2: 31, ORDINAL4:def 1;

      reconsider dA = ( dom A) as Element of NAT by ORDINAL1:def 12;

      

       A4: ( dom A) in ( succ ( dom A)) by ORDINAL1: 6;

      defpred P[ Nat] means $1 in ( succ ( dom A)) implies (f . $1) = (g . $1);

      

       A5: P[ 0 ] by A1, A2;

      

       A6: P[n] implies P[(n + 1)]

      proof

        assume that

         A7: P[n] and

         A8: (n + 1) in ( succ ( dom A));

        ( Segm (n + 1)) = ( succ ( Segm n)) by NAT_1: 38;

        then

         A9: n in ( dom A) by A8, ORDINAL3: 3;

        then n in ( succ ( dom A)) by A4, ORDINAL1: 10;

        then (g . (n + 1)) = ((g . n) +^ (A . n)) & (f . (n + 1)) = ((f . n) +^ ((A ^ <%a%>) . n)) by A1, A2, A3, A9;

        hence thesis by A7, A9, A4, ORDINAL1: 10, ORDINAL4:def 1;

      end;

      

       A10: P[n] from NAT_1:sch 2( A5, A6);

      

      thus ( Sum^ (A ^ <%a%>)) = (f . (( dom A) +^ 1)) by A1, A3, ORDINAL2: 6

      .= (f . (dA + 1)) by CARD_2: 36

      .= ((f . ( dom A)) +^ ((A ^ <%a%>) . ( len A))) by A1, A3, ORDINAL1: 6

      .= ((f . ( dom A)) +^ a) by AFINSQ_1: 36

      .= ((g . ( dom A)) +^ a) by A10, ORDINAL1: 6

      .= (( Sum^ A) +^ a) by A2, ORDINAL2: 6;

    end;

    theorem :: ORDINAL5:55

    

     Th55: for A be finite Ordinal-Sequence holds ( Sum^ ( <%a%> ^ A)) = (a +^ ( Sum^ A))

    proof

      defpred P[ finite Sequence] means for f be finite Ordinal-Sequence st f = $1 holds ( Sum^ ( <%a%> ^ f)) = (a +^ ( Sum^ f));

      ( Sum^ ( <%a%> ^ {} )) = a by Th53;

      then

       A1: P[ {} ] by Th52, ORDINAL2: 27;

      

       A2: for f be finite Sequence, x be object st P[f] holds P[(f ^ <%x%>)]

      proof

        let f be finite Sequence;

        let x be object;

        assume

         A3: P[f];

        let g be finite Ordinal-Sequence;

        consider b such that

         A4: ( rng g) c= b by ORDINAL2:def 4;

        assume

         A5: g = (f ^ <%x%>);

        then ( rng g) = (( rng f) \/ ( rng <%x%>)) by AFINSQ_1: 26;

        then

         A6: ( rng f) c= b & ( rng <%x%>) c= b by A4, XBOOLE_1: 11;

        then

        reconsider f9 = f as finite Ordinal-Sequence by ORDINAL2:def 4;

        ( rng <%x%>) = {x} by AFINSQ_1: 33;

        then x in b by A6, ZFMISC_1: 31;

        then

        reconsider x as Ordinal;

        

        thus ( Sum^ ( <%a%> ^ g)) = ( Sum^ (( <%a%> ^ f9) ^ <%x%>)) by A5, AFINSQ_1: 27

        .= (( Sum^ ( <%a%> ^ f9)) +^ x) by Th54

        .= ((a +^ ( Sum^ f9)) +^ x) by A3

        .= (a +^ (( Sum^ f9) +^ x)) by ORDINAL3: 30

        .= (a +^ ( Sum^ g)) by A5, Th54;

      end;

      for f be finite Sequence holds P[f] from AFINSQ_1:sch 3( A1, A2);

      hence thesis;

    end;

    theorem :: ORDINAL5:56

    

     Th56: for A be finite Ordinal-Sequence holds (A . 0 ) c= ( Sum^ A)

    proof

      let A be finite Ordinal-Sequence;

      defpred P[ finite Sequence] means for A be finite Ordinal-Sequence st $1 = A holds (A . 0 ) c= ( Sum^ A);

      

       A1: P[ {} ];

      

       A2: for f be finite Sequence, x be object st P[f] holds P[(f ^ <%x%>)]

      proof

        let f be finite Sequence;

        let x be object;

        assume

         A3: P[f];

        let g be finite Ordinal-Sequence;

        consider b such that

         A4: ( rng g) c= b by ORDINAL2:def 4;

        assume

         A5: g = (f ^ <%x%>);

        then ( rng g) = (( rng f) \/ ( rng <%x%>)) by AFINSQ_1: 26;

        then

         A6: ( rng f) c= b & ( rng <%x%>) c= b by A4, XBOOLE_1: 11;

        then

        reconsider f9 = f as finite Ordinal-Sequence by ORDINAL2:def 4;

        ( rng <%x%>) = {x} by AFINSQ_1: 33;

        then x in b by A6, ZFMISC_1: 31;

        then

        reconsider x as Ordinal;

        per cases ;

          suppose f = {} ;

          then g = ( {} ^ <%x%>) by A5;

          then g = <%x%>;

          then (g . 0 ) = x & ( Sum^ g) = x by Th53;

          hence (g . 0 ) c= ( Sum^ g);

        end;

          suppose f <> {} ;

          then 0 in ( dom f9) & ( Sum^ g) = (( Sum^ f9) +^ x) by A5, Th54, ORDINAL3: 8;

          then (g . 0 ) = (f9 . 0 ) & (f9 . 0 ) c= ( Sum^ f9) & ( Sum^ f9) c= ( Sum^ g) by A3, A5, ORDINAL3: 24, ORDINAL4:def 1;

          hence (g . 0 ) c= ( Sum^ g);

        end;

      end;

      for f be finite Sequence holds P[f] from AFINSQ_1:sch 3( A1, A2);

      hence (A . 0 ) c= ( Sum^ A);

    end;

    definition

      let a;

      :: ORDINAL5:def9

      attr a is Cantor-component means

      : Def9: ex b, n st 0 in ( Segm n) & a = (n *^ ( exp ( omega ,b)));

    end

    registration

      cluster Cantor-component -> non empty for Ordinal;

      coherence

      proof

        let a;

        given b, n such that

         A1: 0 in ( Segm n) & a = (n *^ ( exp ( omega ,b)));

        ( exp ( omega ,b)) <> 0 by ORDINAL4: 22;

        hence thesis by A1, ORDINAL3: 31;

      end;

    end

    registration

      cluster Cantor-component for Ordinal;

      existence

      proof

        take (1 *^ ( exp ( omega ,1))), 1, 1;

        thus thesis by NAT_1: 44;

      end;

    end

    definition

      let a, b;

      :: ORDINAL5:def10

      func b -exponent (a) -> Ordinal means

      : Def10: ( exp (b,it )) c= a & for c st ( exp (b,c)) c= a holds c c= it if 1 in b & 0 in a

      otherwise it = 0 ;

      existence

      proof

        hereby

          assume

           A1: 1 in b & 0 in a;

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

          a c= ( exp (b,a)) by A1, ORDINAL4: 32;

          then

           A2: ex c st P[c];

          consider c such that

           A3: P[c] & for d st P[d] holds c c= d from ORDINAL1:sch 1( A2);

           0 in ( Segm 1) by NAT_1: 44;

          then

           A4: 0 in b by A1, ORDINAL1: 10;

          per cases by A3;

            suppose

             A5: a = ( exp (b,c));

            take c;

            thus ( exp (b,c)) c= a by A5;

            let d;

            assume

             A6: ( exp (b,d)) c= a & d c/= c;

            then c in d by ORDINAL1: 16;

            then a in ( exp (b,d)) by A1, A5, ORDINAL4: 24;

            then a in a by A6;

            hence contradiction;

          end;

            suppose

             A7: a c< ( exp (b,c));

            then

             A8: a in ( exp (b,c)) by ORDINAL1: 11;

            ( succ 0 ) c= a by A1, ORDINAL1: 21;

            then 1 in ( exp (b,c)) & ( exp (b, 0 )) = 1 by A7, ORDINAL1: 11, ORDINAL1: 12, ORDINAL2: 43;

            then

             A9: c <> 0 ;

            now

              assume c is limit_ordinal;

              then

              consider d such that

               A10: d in c & a in ( exp (b,d)) by A9, A4, A8, Th11;

               P[d] by A10, ORDINAL1:def 2;

              then c c= d by A3;

              then d in d by A10;

              hence contradiction;

            end;

            then

            consider d such that

             A11: c = ( succ d) by ORDINAL1: 29;

            take d;

            thus ( exp (b,d)) c= a

            proof

              assume ( exp (b,d)) c/= a;

              then a c= ( exp (b,d));

              then c c= d by A3;

              then d in d by A11, ORDINAL1: 21;

              hence thesis;

            end;

            let e;

            assume

             A12: ( exp (b,e)) c= a & e c/= d;

            then d in e by ORDINAL1: 16;

            then c c= e by A11, ORDINAL1: 21;

            then ( exp (b,c)) c= ( exp (b,e)) by A1, ORDINAL4: 27;

            then a in ( exp (b,e)) by A8;

            then a in a by A12;

            hence contradiction;

          end;

        end;

        thus thesis;

      end;

      uniqueness ;

      consistency ;

    end

    

     Lm1: 0 in ( Segm 1) by NAT_1: 44;

    theorem :: ORDINAL5:57

    

     Th57: 1 in b implies a in ( exp (b,( succ (b -exponent a))))

    proof

      assume

       A1: 1 in b;

      per cases by ORDINAL3: 8;

        suppose

         A2: 0 in a;

        assume not thesis;

        then ( exp (b,( succ (b -exponent a)))) c= a by ORDINAL1: 16;

        then ( succ (b -exponent a)) c= (b -exponent a) & (b -exponent a) in ( succ (b -exponent a)) by A1, A2, Def10, ORDINAL1: 6;

        then (b -exponent a) in (b -exponent a);

        hence contradiction;

      end;

        suppose

         A3: a = 0 ;

        then (b -exponent a) = 0 by Def10;

        then ( exp (b,( succ (b -exponent a)))) = b by ORDINAL2: 46;

        hence thesis by A1, A3, Lm1, ORDINAL1: 10;

      end;

    end;

    registration

      let a,b be Ordinal;

      cluster <%a, b%> -> Ordinal-yielding;

      coherence

      proof

         <%a, b%> = ( <%a%> ^ <%b%>) by AFINSQ_1:def 5;

        hence thesis;

      end;

      let c be Ordinal;

      cluster <%a, b, c%> -> Ordinal-yielding;

      coherence

      proof

         <%a, b, c%> = (( <%a%> ^ <%b%>) ^ <%c%>) by AFINSQ_1:def 6;

        hence thesis;

      end;

    end

    registration

      let a be non empty Ordinal, b be Ordinal;

      cluster (a +^ b) -> non empty;

      coherence by ORDINAL3: 26;

      cluster (b +^ a) -> non empty;

      coherence by ORDINAL3: 26;

    end

    registration

      let a,b be non empty Ordinal;

      cluster (b *^ a) -> non empty;

      coherence by ORDINAL3: 31;

    end

    registration

      let A be empty Ordinal, B be non empty Ordinal;

      cluster ( exp (A,B)) -> empty;

      coherence by ORDINAL4: 20;

    end

    registration

      let A be Ordinal, B be empty Ordinal;

      cluster ( exp (A,B)) -> non empty;

      coherence by ORDINAL2: 43;

    end

    registration

      let A be non empty Ordinal, B be Ordinal;

      cluster ( exp (A,B)) -> non empty;

      coherence by ORDINAL4: 22;

    end

    theorem :: ORDINAL5:58

    

     Th58: for a,b,c be Ordinal holds 0 in c & c in b implies (b -exponent (c *^ ( exp (b,a)))) = a

    proof

      let a,b,c be Ordinal;

      assume

       A1: 0 in c & c in b;

      then

       A2: ( succ 0 ) c= c by ORDINAL1: 21;

      then

       A3: (1 *^ ( exp (b,a))) = ( exp (b,a)) & (1 *^ ( exp (b,a))) c= (c *^ ( exp (b,a))) by ORDINAL2: 39, ORDINAL2: 41;

      

       A4: 1 in b & 0 in (c *^ ( exp (b,a))) by A2, A1, ORDINAL1: 12, ORDINAL3: 8;

      now

        let d be Ordinal;

        assume

         A5: ( exp (b,d)) c= (c *^ ( exp (b,a))) & d c/= a;

        then ( succ a) c= d by ORDINAL1: 16, ORDINAL1: 21;

        then

         A6: ( exp (b,( succ a))) c= ( exp (b,d)) by A1, ORDINAL4: 27;

        ( exp (b,( succ a))) = (b *^ ( exp (b,a))) by ORDINAL2: 44;

        then (b *^ ( exp (b,a))) c= (c *^ ( exp (b,a))) by A5, A6;

        then b c= c by ORDINAL3: 35;

        then c in c by A1;

        hence contradiction;

      end;

      hence (b -exponent (c *^ ( exp (b,a)))) = a by A3, A4, Def10;

    end;

    theorem :: ORDINAL5:59

    

     Th59: 0 in a & 1 in b & c = (b -exponent a) implies (a div^ ( exp (b,c))) in b

    proof

      assume

       A1: 0 in a & 1 in b & c = (b -exponent a);

      set n = (a div^ ( exp (b,c)));

      ( exp (b,c)) <> 0 by A1;

      then

      consider d such that

       A2: a = ((n *^ ( exp (b,c))) +^ d) & d in ( exp (b,c)) by ORDINAL3:def 6;

      assume not n in b;

      then (b *^ ( exp (b,c))) c= (n *^ ( exp (b,c))) by ORDINAL1: 16, ORDINAL2: 41;

      then ( exp (b,( succ c))) c= (n *^ ( exp (b,c))) & (n *^ ( exp (b,c))) c= a by A2, ORDINAL2: 44, ORDINAL3: 24;

      then ( exp (b,( succ c))) c= a;

      then ( succ c) c= c & c in ( succ c) by A1, Def10, ORDINAL1: 6;

      then c in c;

      hence contradiction;

    end;

    theorem :: ORDINAL5:60

    

     Th60: 0 in a & 1 in b & c = (b -exponent a) implies 0 in (a div^ ( exp (b,c)))

    proof

      assume

       A1: 0 in a & 1 in b & c = (b -exponent a);

      set n = (a div^ ( exp (b,c)));

      ( exp (b,c)) <> 0 by A1;

      then

      consider d such that

       A2: a = ((n *^ ( exp (b,c))) +^ d) & d in ( exp (b,c)) by ORDINAL3:def 6;

      assume not 0 in n;

      then n = 0 by ORDINAL3: 8;

      

      then a = ( 0 qua Ordinal +^ d) by A2, ORDINAL2: 35

      .= d by ORDINAL2: 30;

      then ( exp (b,c)) c= d by A1, Def10;

      then d in d by A2;

      hence contradiction;

    end;

    theorem :: ORDINAL5:61

    

     Th61: b <> 0 implies (a mod^ ( exp (b,c))) in ( exp (b,c))

    proof

      assume that

       A1: b <> 0 ;

      set n = (a div^ ( exp (b,c)));

      ( exp (b,c)) <> 0 by A1;

      then

      consider d such that

       A2: a = ((n *^ ( exp (b,c))) +^ d) & d in ( exp (b,c)) by ORDINAL3:def 6;

      d = (a -^ (n *^ ( exp (b,c)))) by A2, ORDINAL3: 52

      .= (a mod^ ( exp (b,c))) by ORDINAL3:def 7;

      hence thesis by A2;

    end;

    theorem :: ORDINAL5:62

    

     Th62: 0 in a implies ex n, c st a = ((n *^ ( exp ( omega ,( omega -exponent a)))) +^ c) & 0 in ( Segm n) & c in ( exp ( omega ,( omega -exponent a)))

    proof

      assume

       A1: 0 in a;

      set c = ( omega -exponent a);

      set n = (a div^ ( exp ( omega ,c)));

      set b = (a mod^ ( exp ( omega ,c)));

      n in omega by A1, Th59;

      then

      reconsider n as Nat;

      take n, b;

      thus a = ((n *^ ( exp ( omega ,c))) +^ b) by ORDINAL3: 65;

      thus 0 in ( Segm n) by A1, Th60;

      thus b in ( exp ( omega ,c)) by Th61;

    end;

    theorem :: ORDINAL5:63

    

     Th63: 1 in c & (c -exponent b) in (c -exponent a) implies b in a

    proof

      assume

       A1: 1 in c & (c -exponent b) in (c -exponent a);

      then ( succ (c -exponent b)) c= (c -exponent a) by ORDINAL1: 21;

      then

       A2: ( exp (c,( succ (c -exponent b)))) c= ( exp (c,(c -exponent a))) by A1, ORDINAL4: 27;

      

       A3: 0 in a by A1, Def10;

      b in ( exp (c,( succ (c -exponent b)))) by A1, Th57;

      then b in ( exp (c,(c -exponent a))) & ( exp (c,(c -exponent a))) c= a by A1, A2, A3, Def10;

      hence thesis;

    end;

    definition

      let A be Ordinal-Sequence;

      :: ORDINAL5:def11

      attr A is Cantor-normal-form means

      : Def11: (for a st a in ( dom A) holds (A . a) is Cantor-component) & for a, b st a in b & b in ( dom A) holds ( omega -exponent (A . b)) in ( omega -exponent (A . a));

    end

    registration

      cluster empty -> Cantor-normal-form for Ordinal-Sequence;

      coherence ;

      cluster Cantor-normal-form -> non-empty for Ordinal-Sequence;

      coherence

      proof

        let A be Ordinal-Sequence;

        assume

         A1: A is Cantor-normal-form;

        now

          let x be object;

          assume x in ( dom A);

          then (A . x) is Cantor-component by A1;

          hence (A . x) is non empty;

        end;

        hence thesis by FUNCT_1:def 9;

      end;

      cluster Cantor-normal-form -> decreasing for Ordinal-Sequence;

      coherence

      proof

        let f such that for a st a in ( dom f) holds (f . a) is Cantor-component and

         A1: for a, b st a in b & b in ( dom f) holds ( omega -exponent (f . b)) in ( omega -exponent (f . a));

        let a, b;

        assume a in b & b in ( dom f);

        then ( omega -exponent (f . b)) in ( omega -exponent (f . a)) by A1;

        hence thesis by Th63;

      end;

    end

    reserve A,B for Cantor-normal-form Ordinal-Sequence;

    theorem :: ORDINAL5:64

    ( Sum^ A) = 0 implies A = {}

    proof

      assume

       A1: ( Sum^ A) = 0 & A <> {} ;

      then 0 in ( dom A) by ORDINAL3: 8;

      then

      reconsider a = (A . 0 ) as Cantor-component Ordinal by Def11;

       0 in a & a c= ( Sum^ A) by Th56, ORDINAL3: 8;

      hence thesis by A1;

    end;

    theorem :: ORDINAL5:65

    

     Th65: 0 in ( Segm n) implies <%(n *^ ( exp ( omega ,b)))%> is Cantor-normal-form

    proof

      assume

       A1: 0 in ( Segm n);

      set A = <%(n *^ ( exp ( omega ,b)))%>;

      

       A2: ( dom A) = ( Segm 1) & (A . 0 ) = (n *^ ( exp ( omega ,b))) by AFINSQ_1:def 4;

      hereby

        let a;

        assume a in ( dom A);

        then a = 0 & 0 in ( Segm 1) by A2, ORDINAL3: 15, TARSKI:def 1;

        hence (A . a) is Cantor-component by A1;

      end;

      let a, b;

      assume

       A3: a in b;

      assume b in ( dom A);

      hence ( omega -exponent (A . b)) in ( omega -exponent (A . a)) by A3, A2, ORDINAL3: 15, TARSKI:def 1;

    end;

    registration

      cluster non empty Cantor-normal-form for Ordinal-Sequence;

      existence

      proof

        take A = <%(1 *^ ( exp ( omega ,1)))%>;

        thus A is non empty;

         0 in ( Segm 1) by NAT_1: 44;

        hence thesis by Th65;

      end;

    end

    theorem :: ORDINAL5:66

    

     Th66: for A,B be Ordinal-Sequence st (A ^ B) is Cantor-normal-form holds A is Cantor-normal-form & B is Cantor-normal-form

    proof

      let A,B be Ordinal-Sequence;

      set AB = (A ^ B);

      assume that

       A1: for a st a in ( dom (A ^ B)) holds ((A ^ B) . a) is Cantor-component and

       A2: for a, b st a in b & b in ( dom (A ^ B)) holds ( omega -exponent ((A ^ B) . b)) in ( omega -exponent ((A ^ B) . a));

      

       A3: ( dom (A ^ B)) = (( dom A) +^ ( dom B)) by ORDINAL4:def 1;

      then

       A4: ( dom A) c= ( dom (A ^ B)) by ORDINAL3: 24;

      thus A is Cantor-normal-form

      proof

        hereby

          let a;

          assume a in ( dom A);

          then (A . a) = ((A ^ B) . a) & a in ( dom (A ^ B)) by A4, ORDINAL4:def 1;

          hence (A . a) is Cantor-component by A1;

        end;

        let a, b;

        assume

         A5: a in b & b in ( dom A);

        then a in ( dom A) by ORDINAL1: 10;

        then (A . a) = (AB . a) & (A . b) = (AB . b) & b in ( dom AB) by A4, A5, ORDINAL4:def 1;

        hence ( omega -exponent (A . b)) in ( omega -exponent (A . a)) by A2, A5;

      end;

      hereby

        let a;

        assume a in ( dom B);

        then (B . a) = (AB . (( dom A) +^ a)) & (( dom A) +^ a) in ( dom AB) by A3, ORDINAL3: 17, ORDINAL4:def 1;

        hence (B . a) is Cantor-component by A1;

      end;

      let a, b;

      assume

       A6: a in b & b in ( dom B);

      then a in ( dom B) by ORDINAL1: 10;

      then (B . a) = (AB . (( dom A) +^ a)) & (B . b) = (AB . (( dom A) +^ b)) & (( dom A) +^ b) in ( dom AB) & (( dom A) +^ a) in (( dom A) +^ b) by A3, A6, ORDINAL3: 17, ORDINAL4:def 1;

      hence ( omega -exponent (B . b)) in ( omega -exponent (B . a)) by A2;

    end;

    theorem :: ORDINAL5:67

    A <> {} implies ex c be Cantor-component Ordinal, B st A = ( <%c%> ^ B)

    proof

      assume A <> {} ;

      then

      consider n be Nat such that

       A1: ( len A) = (n + 1) by NAT_1: 6;

      reconsider n as Element of NAT by ORDINAL1:def 12;

      (n + 1) = (1 +^ n) by CARD_2: 36;

      then

      consider S1, S2 such that

       A2: A = (S1 ^ S2) & ( dom S1) = 1 & ( dom S2) = n by A1, Th2;

      reconsider S1, S2 as Ordinal-Sequence by A2, Th4;

      (S1 ^ S2) is Cantor-normal-form by A2;

      then

      reconsider S1, S2 as Cantor-normal-form Ordinal-Sequence by Th66;

       0 in ( Segm 1) by NAT_1: 44;

      then

      reconsider c = (S1 . 0 ) as Cantor-component Ordinal by A2, Def11;

      take c, S2;

      ( len S1) = 1 by A2;

      hence thesis by A2, AFINSQ_1: 34;

    end;

    theorem :: ORDINAL5:68

    

     Th68: for A be non empty Cantor-normal-form Ordinal-Sequence holds for c be Cantor-component Ordinal st ( omega -exponent (A . 0 )) in ( omega -exponent c) holds ( <%c%> ^ A) is Cantor-normal-form

    proof

      let A be non empty Cantor-normal-form Ordinal-Sequence;

      let c be Cantor-component Ordinal such that

       A1: ( omega -exponent (A . 0 )) in ( omega -exponent c);

      set B = ( <%c%> ^ A);

      

       A2: ( dom <%c%>) = 1 & ( <%c%> . 0 ) = c by AFINSQ_1:def 4;

      then

       A3: ( dom B) = (1 +^ ( dom A)) by ORDINAL4:def 1;

      hereby

        let a;

        assume

         A4: a in ( dom B);

        per cases by A3, A4, ORDINAL3: 38;

          suppose

           A5: a in 1;

          then a = 0 by ORDINAL3: 15, TARSKI:def 1;

          hence (B . a) is Cantor-component by A2, A5, ORDINAL4:def 1;

        end;

          suppose ex b st b in ( dom A) & a = (1 +^ b);

          then

          consider b such that

           A6: b in ( dom A) & a = (1 +^ b);

          (B . a) = (A . b) by A2, A6, ORDINAL4:def 1;

          hence (B . a) is Cantor-component by A6, Def11;

        end;

      end;

      let a, b;

      assume

       A7: a in b & b in ( dom B);

      per cases ;

        suppose not a in 1;

        then

         A8: 1 c= a by ORDINAL1: 16;

        then

         A9: 1 in b & a in ( dom B) & ((1 +^ ( dom A)) -^ 1) = ( dom A) by A7, ORDINAL1: 10, ORDINAL1: 12, ORDINAL3: 52;

        then

         A10: (b -^ 1) in ( dom A) & (a -^ 1) in ( dom A) & (a -^ 1) in (b -^ 1) by A8, A3, A7, ORDINAL3: 53;

        b = (1 +^ (b -^ 1)) & a = (1 +^ (a -^ 1)) by A8, A9, ORDINAL3: 51, ORDINAL3:def 5;

        then (B . a) = (A . (a -^ 1)) & (B . b) = (A . (b -^ 1)) by A2, A10, ORDINAL4:def 1;

        hence thesis by A10, Def11;

      end;

        suppose a in 1;

        then

         A11: (B . a) = ( <%c%> . a) & a = 0 by A2, ORDINAL3: 15, ORDINAL4:def 1, TARSKI:def 1;

        then

         A12: ( succ 0 ) c= b by A7, ORDINAL1: 21;

        then (b -^ 1) in ((1 +^ ( dom A)) -^ 1) by A3, A7, ORDINAL3: 53;

        then

         A13: (b -^ 1) in ( dom A) & b = (1 +^ (b -^ 1)) by A12, ORDINAL3: 52, ORDINAL3:def 5;

        then

         A14: (B . b) = (A . (b -^ 1)) by A2, ORDINAL4:def 1;

         0 in ( dom A) & ((b -^ 1) = 0 or 0 in (b -^ 1)) by ORDINAL3: 8;

        then ( omega -exponent (A . 0 )) = ( omega -exponent (A . (b -^ 1))) or ( omega -exponent (A . (b -^ 1))) in ( omega -exponent (A . 0 )) by A13, Def11;

        hence thesis by A1, A11, A14, ORDINAL1: 10;

      end;

    end;

    ::$Notion-Name

    theorem :: ORDINAL5:69

    ex A be Cantor-normal-form Ordinal-Sequence st a = ( Sum^ A)

    proof

      defpred P[ Ordinal] means 0 in $1 implies ex A be non empty Cantor-normal-form Ordinal-Sequence st $1 = ( Sum^ A);

      

       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 P[b] and

         A3: 0 in a;

        consider n, b such that

         A4: a = ((n *^ ( exp ( omega ,( omega -exponent a)))) +^ b) & 0 in ( Segm n) & b in ( exp ( omega ,( omega -exponent a))) by A3, Th62;

        reconsider s = (n *^ ( exp ( omega ,( omega -exponent a)))) as Cantor-component Ordinal by A4, Def9;

        set c = ( omega -exponent a);

        

         A5: ( exp ( omega ,c)) c= a by A3, Def10;

        per cases by ORDINAL3: 8;

          suppose

           A6: b = 0 ;

          reconsider A = <%(n *^ ( exp ( omega ,( omega -exponent a))))%> as non empty Cantor-normal-form Ordinal-Sequence by A4, Th65;

          take A;

          

          thus a = (n *^ ( exp ( omega ,( omega -exponent a)))) by A4, A6, ORDINAL2: 27

          .= ( Sum^ A) by Th53;

        end;

          suppose 0 in b;

          then

          consider A be non empty Cantor-normal-form Ordinal-Sequence such that

           A7: b = ( Sum^ A) by A5, A2, A4;

          

           A8: (A . 0 ) in ( exp ( omega ,( omega -exponent a))) by A4, A7, Th56, ORDINAL1: 12;

           0 in ( dom A) by ORDINAL3: 8;

          then (A . 0 ) is Cantor-component Ordinal by Def11;

          then 0 in (A . 0 ) by ORDINAL3: 8;

          then ( exp ( omega ,( omega -exponent (A . 0 )))) c= (A . 0 ) by Def10;

          then

           A9: ( exp ( omega ,( omega -exponent (A . 0 )))) in ( exp ( omega ,( omega -exponent a))) by A8, ORDINAL1: 12;

          n in omega by ORDINAL1:def 12;

          then ( omega -exponent s) = ( omega -exponent a) by A4, Th58;

          then

          reconsider B = ( <%s%> ^ A) as non empty Cantor-normal-form Ordinal-Sequence by A9, Th68, Th12;

          take B;

          thus a = ( Sum^ B) by A4, A7, Th55;

        end;

      end;

      

       A10: P[b] from ORDINAL1:sch 2( A1);

      per cases by ORDINAL3: 8;

        suppose

         A11: a = 0 ;

        reconsider A = {} as Cantor-normal-form Ordinal-Sequence;

        take A;

        thus thesis by A11, Th52;

      end;

        suppose 0 in a;

        then ex A be non empty Cantor-normal-form Ordinal-Sequence st a = ( Sum^ A) by A10;

        hence thesis;

      end;

    end;