ordinal4.miz



    begin

    reserve phi,fi,psi for Ordinal-Sequence,

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

f,g for Function,

X for set,

x,y,z for object;

    

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

    

     Lm2: omega is limit_ordinal by ORDINAL1:def 11;

    

     Lm3: 1 = ( succ {} );

    registration

      let L be Ordinal-Sequence;

      cluster ( last L) -> ordinal;

      coherence ;

    end

    theorem :: ORDINAL4:1

    ( dom fi) = ( succ A) implies ( last fi) is_limes_of fi & ( lim fi) = ( last fi)

    proof

      assume

       A1: ( dom fi) = ( succ A);

      then

       A2: ( last fi) = (fi . A) by ORDINAL2: 6;

      thus ( last fi) is_limes_of fi

      proof

        per cases ;

          case

           A3: ( last fi) = 0 ;

          take A;

          thus A in ( dom fi) by A1, ORDINAL1: 6;

          let B;

          assume that

           A4: A c= B and

           A5: B in ( dom fi);

          B c= A by A1, A5, ORDINAL1: 22;

          hence thesis by A2, A3, A4, XBOOLE_0:def 10;

        end;

          case ( last fi) <> 0 ;

          let B, C such that

           A6: B in ( last fi) and

           A7: ( last fi) in C;

          take A;

          thus A in ( dom fi) by A1, ORDINAL1: 6;

          let D;

          assume that

           A8: A c= D and

           A9: D in ( dom fi);

          D c= A by A1, A9, ORDINAL1: 22;

          hence thesis by A2, A6, A7, A8, XBOOLE_0:def 10;

        end;

      end;

      hence thesis by ORDINAL2:def 10;

    end;

    definition

      let fi,psi be Sequence;

      :: ORDINAL4:def1

      func fi ^ psi -> Sequence means

      : Def1: ( dom it ) = (( dom fi) +^ ( dom psi)) & (for A st A in ( dom fi) holds (it . A) = (fi . A)) & for A st A in ( dom psi) holds (it . (( dom fi) +^ A)) = (psi . A);

      existence

      proof

        defpred P[ set] means $1 in ( dom fi);

        deffunc G( Ordinal) = (psi . ($1 -^ ( dom fi)));

        deffunc F( set) = (fi . $1);

        consider f such that

         A1: ( dom f) = (( dom fi) +^ ( dom psi)) and

         A2: for x be Ordinal st x in (( dom fi) +^ ( dom psi)) holds ( P[x] implies (f . x) = F(x)) & ( not P[x] implies (f . x) = G(x)) from FINSET_1:sch 1;

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

        take f;

        thus ( dom f) = (( dom fi) +^ ( dom psi)) by A1;

        thus for A st A in ( dom fi) holds (f . A) = (fi . A)

        proof

          

           A3: ( dom fi) c= ( dom f) by A1, ORDINAL3: 24;

          let A;

          assume A in ( dom fi);

          hence thesis by A1, A2, A3;

        end;

        let A;

        ( dom fi) c= (( dom fi) +^ A) by ORDINAL3: 24;

        then

         A4: not (( dom fi) +^ A) in ( dom fi) by ORDINAL1: 5;

        assume A in ( dom psi);

        then (( dom fi) +^ A) in ( dom f) by A1, ORDINAL2: 32;

        then (f . (( dom fi) +^ A)) = (psi . ((( dom fi) +^ A) -^ ( dom fi))) by A1, A2, A4;

        hence thesis by ORDINAL3: 52;

      end;

      uniqueness

      proof

        let f1,f2 be Sequence such that

         A5: ( dom f1) = (( dom fi) +^ ( dom psi)) and

         A6: for A st A in ( dom fi) holds (f1 . A) = (fi . A) and

         A7: for A st A in ( dom psi) holds (f1 . (( dom fi) +^ A)) = (psi . A) and

         A8: ( dom f2) = (( dom fi) +^ ( dom psi)) and

         A9: for A st A in ( dom fi) holds (f2 . A) = (fi . A) and

         A10: for A st A in ( dom psi) holds (f2 . (( dom fi) +^ A)) = (psi . A);

        now

          let x be object;

          assume

           A11: x in (( dom fi) +^ ( dom psi));

          then

          reconsider A = x as Ordinal;

          now

            per cases ;

              suppose

               A12: x in ( dom fi);

              then (f1 . A) = (fi . A) by A6;

              hence (f1 . x) = (f2 . x) by A9, A12;

            end;

              suppose not x in ( dom fi);

              then ( dom fi) c= A by ORDINAL1: 16;

              then

               A13: (( dom fi) +^ (A -^ ( dom fi))) = A by ORDINAL3:def 5;

              then (f1 . A) = (psi . (A -^ ( dom fi))) by A7, A11, ORDINAL3: 22;

              hence (f1 . x) = (f2 . x) by A10, A11, A13, ORDINAL3: 22;

            end;

          end;

          hence (f1 . x) = (f2 . x);

        end;

        hence thesis by A5, A8, FUNCT_1: 2;

      end;

    end

    

     Th2Lem: for fi,psi be Sequence holds ( rng (fi ^ psi)) c= (( rng fi) \/ ( rng psi))

    proof

      let fi,psi be Sequence;

      set f = (fi ^ psi), A1 = ( rng fi), A2 = ( rng psi);

      

       A1: ( dom (fi ^ psi)) = (( dom fi) +^ ( dom psi)) by Def1;

      let y be object;

      assume y in ( rng f);

      then

      consider x be object such that

       A2: x in ( dom f) and

       A3: y = (f . x) by FUNCT_1:def 3;

      reconsider x as Ordinal by A2;

      per cases ;

        suppose

         A4: x in ( dom fi);

        then

         A5: (fi . x) in ( rng fi) by FUNCT_1:def 3;

        y = (fi . x) by A3, A4, Def1;

        then y in A1 by A5;

        hence thesis by XBOOLE_0:def 3;

      end;

        suppose not x in ( dom fi);

        then ( dom fi) c= x by ORDINAL1: 16;

        then

         A6: (( dom fi) +^ (x -^ ( dom fi))) = x by ORDINAL3:def 5;

        then

         A7: (x -^ ( dom fi)) in ( dom psi) by A1, A2, ORDINAL3: 22;

        then y = (psi . (x -^ ( dom fi))) by A3, A6, Def1;

        then y in ( rng psi) by A7, FUNCT_1:def 3;

        then y in A2;

        hence thesis by XBOOLE_0:def 3;

      end;

    end;

    

     Th7A: for A,B be Sequence holds ( rng A) c= ( rng (A ^ B))

    proof

      let A,B be Sequence;

      let y be object;

      assume y in ( rng A);

      then

      consider x be object such that

       A1: x in ( dom A) & (A . x) = y by FUNCT_1:def 3;

      

       A2: ((A ^ B) . x) = y by A1, Def1;

      ( dom A) c= (( dom A) +^ ( dom B)) by ORDINAL3: 24;

      then ( dom A) c= ( dom (A ^ B)) by Def1;

      hence y in ( rng (A ^ B)) by A1, A2, FUNCT_1: 3;

    end;

    

     Th8A: for A,B be Sequence holds ( rng B) c= ( rng (A ^ B))

    proof

      let A,B be Sequence;

      let y be object;

      assume y in ( rng B);

      then

      consider x be object such that

       A1: x in ( dom B) & (B . x) = y by FUNCT_1:def 3;

      reconsider x as Ordinal by A1;

      

       A2: ((A ^ B) . (( dom A) +^ x)) = y by A1, Def1;

      (( dom A) +^ x) in (( dom A) +^ ( dom B)) by A1, ORDINAL2: 32;

      then (( dom A) +^ x) in ( dom (A ^ B)) by Def1;

      hence y in ( rng (A ^ B)) by A2, FUNCT_1: 3;

    end;

    theorem :: ORDINAL4:2

    

     Th2: for A,B be Sequence holds ( rng (A ^ B)) = (( rng A) \/ ( rng B))

    proof

      let A,B be Sequence;

      ( rng A) c= ( rng (A ^ B)) & ( rng B) c= ( rng (A ^ B)) by Th7A, Th8A;

      then

       A1: (( rng A) \/ ( rng B)) c= ( rng (A ^ B)) by XBOOLE_1: 8;

      ( rng (A ^ B)) c= (( rng A) \/ ( rng B)) by Th2Lem;

      hence thesis by A1;

    end;

    registration

      let fi, psi;

      cluster (fi ^ psi) -> Ordinal-yielding;

      coherence

      proof

        set f = (fi ^ psi);

        consider A1 be Ordinal such that

         A1: ( rng fi) c= A1 by ORDINAL2:def 4;

        consider A2 be Ordinal such that

         A2: ( rng psi) c= A2 by ORDINAL2:def 4;

        

         A3: A2 c= (A1 +^ A2) by ORDINAL3: 24;

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

        then

         A4: (A1 \/ A2) c= (A1 +^ A2) by A3, XBOOLE_1: 8;

        

         A5: ( rng f) c= (( rng fi) \/ ( rng psi)) by Th2;

        (( rng fi) \/ ( rng psi)) c= (A1 \/ A2) by A1, A2, XBOOLE_1: 13;

        then ( rng f) c= (A1 \/ A2) by A5;

        then ( rng f) c= (A1 +^ A2) by A4;

        hence thesis;

      end;

    end

    theorem :: ORDINAL4:3

    

     Th3: A is_limes_of psi implies A is_limes_of (fi ^ psi)

    proof

      assume that

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

      

       A2: ( dom (fi ^ psi)) = (( dom fi) +^ ( dom psi)) by Def1;

      per cases ;

        case A = 0 ;

        then

        consider B such that

         A3: B in ( dom psi) and

         A4: for C st B c= C & C in ( dom psi) holds (psi . C) = {} by A1;

        take B1 = (( dom fi) +^ B);

        thus B1 in ( dom (fi ^ psi)) by A2, A3, ORDINAL2: 32;

        let C;

        assume that

         A5: B1 c= C and

         A6: C in ( dom (fi ^ psi));

        

         A7: C = (B1 +^ (C -^ B1)) by A5, ORDINAL3:def 5

        .= (( dom fi) +^ (B +^ (C -^ B1))) by ORDINAL3: 30;

        then

         A8: (B +^ (C -^ B1)) in ( dom psi) by A2, A6, ORDINAL3: 22;

        B c= (B +^ (C -^ B1)) by ORDINAL3: 24;

        then (psi . (B +^ (C -^ B1))) = {} by A2, A4, A6, A7, ORDINAL3: 22;

        hence thesis by A7, A8, Def1;

      end;

        case A <> 0 ;

        let B, C;

        assume that

         A9: B in A and

         A10: A in C;

        consider D such that

         A11: D in ( dom psi) and

         A12: for E be Ordinal st D c= E & E in ( dom psi) holds B in (psi . E) & (psi . E) in C by A1, A9, A10;

        take D1 = (( dom fi) +^ D);

        thus D1 in ( dom (fi ^ psi)) by A2, A11, ORDINAL2: 32;

        let E be Ordinal;

        assume that

         A13: D1 c= E and

         A14: E in ( dom (fi ^ psi));

        

         A15: D c= (D +^ (E -^ D1)) by ORDINAL3: 24;

        

         A16: E = (D1 +^ (E -^ D1)) by A13, ORDINAL3:def 5

        .= (( dom fi) +^ (D +^ (E -^ D1))) by ORDINAL3: 30;

        then

         A17: (D +^ (E -^ D1)) in ( dom psi) by A2, A14, ORDINAL3: 22;

        then ((fi ^ psi) . E) = (psi . (D +^ (E -^ D1))) by A16, Def1;

        hence thesis by A12, A15, A17;

      end;

    end;

    theorem :: ORDINAL4:4

    A is_limes_of fi implies (B +^ A) is_limes_of (B +^ fi)

    proof

      assume that

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

      

       A2: ( dom fi) = ( dom (B +^ fi)) by ORDINAL3:def 1;

      per cases ;

        case

         A3: (B +^ A) = 0 ;

        then

        consider A1 such that

         A4: A1 in ( dom fi) and

         A5: for C st A1 c= C & C in ( dom fi) holds (fi . C) = {} by A1, ORDINAL3: 26;

        take A1;

        thus A1 in ( dom (B +^ fi)) by A4, ORDINAL3:def 1;

        let C;

        assume that

         A6: A1 c= C and

         A7: C in ( dom (B +^ fi));

        

         A8: ((B +^ fi) . C) = (B +^ (fi . C)) by A2, A7, ORDINAL3:def 1;

        (fi . C) = {} by A2, A5, A6, A7;

        hence thesis by A3, A8, ORDINAL3: 26;

      end;

        case (B +^ A) <> 0 ;

        now

          per cases ;

            suppose

             A9: A = {} ;

            then

            consider A1 such that

             A10: A1 in ( dom fi) and

             A11: for C st A1 c= C & C in ( dom fi) holds (fi . C) = {} by A1;

            let B1,B2 be Ordinal such that

             A12: B1 in (B +^ A) and

             A13: (B +^ A) in B2;

            take A1;

            thus A1 in ( dom (B +^ fi)) by A10, ORDINAL3:def 1;

            let C;

            assume that

             A14: A1 c= C and

             A15: C in ( dom (B +^ fi));

            ((B +^ fi) . C) = (B +^ (fi . C)) by A2, A15, ORDINAL3:def 1;

            hence B1 in ((B +^ fi) . C) & ((B +^ fi) . C) in B2 by A2, A9, A11, A12, A13, A14, A15;

          end;

            suppose

             A16: A <> {} ;

            let B1,B2 be Ordinal;

            assume that

             A17: B1 in (B +^ A) and

             A18: (B +^ A) in B2;

            (B1 -^ B) in A by A16, A17, ORDINAL3: 60;

            then

            consider A1 such that

             A19: A1 in ( dom fi) and

             A20: for C st A1 c= C & C in ( dom fi) holds (B1 -^ B) in (fi . C) & (fi . C) in (B2 -^ B) by A1, A18, ORDINAL3: 61;

            

             A21: B1 c= (B +^ (B1 -^ B)) by ORDINAL3: 62;

            

             A22: B c= (B +^ A) by ORDINAL3: 24;

            (B +^ A) c= B2 by A18, ORDINAL1:def 2;

            then B c= B2 by A22;

            then

             A23: (B +^ (B2 -^ B)) = B2 by ORDINAL3:def 5;

            take A1;

            thus A1 in ( dom (B +^ fi)) by A19, ORDINAL3:def 1;

            let C;

            assume that

             A24: A1 c= C and

             A25: C in ( dom (B +^ fi));

            

             A26: ((B +^ fi) . C) = (B +^ (fi . C)) by A2, A25, ORDINAL3:def 1;

            reconsider E = (fi . C) as Ordinal;

            (B1 -^ B) in E by A2, A20, A24, A25;

            then

             A27: (B +^ (B1 -^ B)) in (B +^ E) by ORDINAL2: 32;

            E in (B2 -^ B) by A2, A20, A24, A25;

            hence B1 in ((B +^ fi) . C) & ((B +^ fi) . C) in B2 by A21, A26, A23, A27, ORDINAL1: 12, ORDINAL2: 32;

          end;

        end;

        hence thesis;

      end;

    end;

    

     Lm4: A is_limes_of fi implies ( dom fi) <> {}

    proof

      assume that

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

      now

        per cases ;

          suppose A = {} ;

          hence thesis by A1;

        end;

          suppose A <> {} ;

          then {} in A by ORDINAL3: 8;

          then ex B st B in ( dom fi) & for C st B c= C & C in ( dom fi) holds {} in (fi . C) & (fi . C) in ( succ A) by A1, ORDINAL1: 6;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: ORDINAL4:5

    

     Th5: A is_limes_of fi implies (A *^ B) is_limes_of (fi *^ B)

    proof

      

       A1: ( dom fi) = ( dom (fi *^ B)) by ORDINAL3:def 4;

      assume

       A2: A is_limes_of fi;

      then

       A3: ( dom fi) <> {} by Lm4;

      per cases ;

        case (A *^ B) = 0 ;

        then

         A4: B = {} or A = {} by ORDINAL3: 31;

        now

          per cases ;

            suppose

             A5: B = {} ;

            set x = the Element of ( dom fi);

            reconsider x as Ordinal;

            take A1 = x;

            thus A1 in ( dom (fi *^ B)) by A1, A3;

            let C;

            assume that A1 c= C and

             A6: C in ( dom (fi *^ B));

            

            thus ((fi *^ B) . C) = ((fi . C) *^ B) by A1, A6, ORDINAL3:def 4

            .= {} by A5, ORDINAL2: 38;

          end;

            suppose B <> {} ;

            then

            consider A1 such that

             A7: A1 in ( dom fi) and

             A8: for C st A1 c= C & C in ( dom fi) holds (fi . C) = {} by A2, A4, ORDINAL2:def 9;

            take A1;

            thus A1 in ( dom (fi *^ B)) by A7, ORDINAL3:def 4;

            let C;

            assume that

             A9: A1 c= C and

             A10: C in ( dom (fi *^ B));

            

             A11: ((fi *^ B) . C) = ((fi . C) *^ B) by A1, A10, ORDINAL3:def 4;

            (fi . C) = {} by A1, A8, A9, A10;

            hence ((fi *^ B) . C) = {} by A11, ORDINAL2: 35;

          end;

        end;

        hence thesis;

      end;

        case

         A12: (A *^ B) <> 0 ;

        let B1,B2 be Ordinal such that

         A13: B1 in (A *^ B) and

         A14: (A *^ B) in B2;

        

         A15: B <> {} by A12, ORDINAL2: 38;

         A16:

        now

          assume not ex A1 st A = ( succ A1);

          then A is limit_ordinal by ORDINAL1: 29;

          then

          consider C such that

           A17: C in A and

           A18: B1 in (C *^ B) by A13, ORDINAL3: 41;

          A in ( succ A) by ORDINAL1: 6;

          then

          consider D such that

           A19: D in ( dom fi) and

           A20: for A1 st D c= A1 & A1 in ( dom fi) holds C in (fi . A1) & (fi . A1) in ( succ A) by A2, A17, ORDINAL2:def 9;

          take D;

          thus D in ( dom (fi *^ B)) by A19, ORDINAL3:def 4;

          let A1;

          assume that

           A21: D c= A1 and

           A22: A1 in ( dom (fi *^ B));

          reconsider E = (fi . A1) as Ordinal;

          (fi . A1) in ( succ A) by A1, A20, A21, A22;

          then

           A23: E c= A by ORDINAL1: 22;

          C in (fi . A1) by A1, A20, A21, A22;

          then (C *^ B) in (E *^ B) by A15, ORDINAL2: 40;

          then

           A24: B1 in (E *^ B) by A18, ORDINAL1: 10;

          ((fi *^ B) . A1) = ((fi . A1) *^ B) by A1, A22, ORDINAL3:def 4;

          hence B1 in ((fi *^ B) . A1) & ((fi *^ B) . A1) in B2 by A14, A23, A24, ORDINAL1: 12, ORDINAL2: 41;

        end;

        now

          

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

          given A1 such that

           A26: A = ( succ A1);

          A1 in A by A26, ORDINAL1: 6;

          then

          consider D such that

           A27: D in ( dom fi) and

           A28: for C st D c= C & C in ( dom fi) holds A1 in (fi . C) & (fi . C) in ( succ A) by A2, A25, ORDINAL2:def 9;

          take D;

          thus D in ( dom (fi *^ B)) by A27, ORDINAL3:def 4;

          let C;

          assume that

           A29: D c= C and

           A30: C in ( dom (fi *^ B));

          reconsider E = (fi . C) as Ordinal;

          A1 in E by A1, A28, A29, A30;

          then

           A31: A c= E by A26, ORDINAL1: 21;

          E in ( succ A) by A1, A28, A29, A30;

          then

           A32: E c= A by ORDINAL1: 22;

          ((fi *^ B) . C) = (E *^ B) by A1, A30, ORDINAL3:def 4;

          hence B1 in ((fi *^ B) . C) & ((fi *^ B) . C) in B2 by A13, A14, A31, A32, XBOOLE_0:def 10;

        end;

        hence thesis by A16;

      end;

    end;

    theorem :: ORDINAL4:6

    

     Th6: ( dom fi) = ( dom psi) & B is_limes_of fi & C is_limes_of psi & ((for A st A in ( dom fi) holds (fi . A) c= (psi . A)) or for A st A in ( dom fi) holds (fi . A) in (psi . A)) implies B c= C

    proof

      assume that

       A1: ( dom fi) = ( dom psi) and

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

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

       A4: (for A st A in ( dom fi) holds (fi . A) c= (psi . A)) or for A st A in ( dom fi) holds (fi . A) in (psi . A);

      

       A5: for A st A in ( dom fi) holds (fi . A) c= (psi . A) by A4, ORDINAL1:def 2;

      now

        per cases ;

          suppose B = {} & C = {} ;

          hence thesis;

        end;

          suppose B = {} & C <> {} ;

          then B in C by ORDINAL3: 8;

          hence thesis by ORDINAL1:def 2;

        end;

          suppose

           A6: B <> {} & C = {} ;

          then {} in B by ORDINAL3: 8;

          then

          consider A2 be Ordinal such that

           A7: A2 in ( dom fi) and

           A8: for A st A2 c= A & A in ( dom fi) holds {} in (fi . A) & (fi . A) in ( succ B) by A2, ORDINAL1: 6;

          consider A1 such that

           A9: A1 in ( dom psi) and

           A10: for A st A1 c= A & A in ( dom psi) holds (psi . A) = {} by A3, A6;

          

           A11: (A1 \/ A2) = A1 or (A1 \/ A2) = A2 by ORDINAL3: 12;

          then

           A12: (fi . (A1 \/ A2)) c= (psi . (A1 \/ A2)) by A1, A5, A9, A7;

          A2 c= (A1 \/ A2) by XBOOLE_1: 7;

          then {} in (fi . (A1 \/ A2)) by A1, A9, A7, A8, A11;

          hence thesis by A1, A9, A10, A7, A11, A12, XBOOLE_1: 7;

        end;

          suppose

           A13: B <> {} & C <> {} ;

          assume not B c= C;

          then C in B by ORDINAL1: 16;

          then

          consider A1 such that

           A14: A1 in ( dom fi) and

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

           {} in C by A13, ORDINAL3: 8;

          then

          consider A2 be Ordinal such that

           A16: A2 in ( dom psi) and

           A17: for A st A2 c= A & A in ( dom psi) holds {} in (psi . A) & (psi . A) in ( succ C) by A3, ORDINAL1: 6;

          

           A18: (A1 \/ A2) = A1 or (A1 \/ A2) = A2 by ORDINAL3: 12;

          reconsider A3 = (psi . (A1 \/ A2)) as Ordinal;

          A2 c= (A1 \/ A2) by XBOOLE_1: 7;

          then (psi . (A1 \/ A2)) in ( succ C) by A1, A14, A16, A17, A18;

          then

           A19: A3 c= C by ORDINAL1: 22;

          A1 c= (A1 \/ A2) by XBOOLE_1: 7;

          then

           A20: C in (fi . (A1 \/ A2)) by A1, A14, A15, A16, A18;

          (fi . (A1 \/ A2)) c= (psi . (A1 \/ A2)) by A1, A5, A14, A16, A18;

          hence contradiction by A20, A19, ORDINAL1: 5;

        end;

      end;

      hence thesis;

    end;

    reserve f1,f2 for Ordinal-Sequence;

    theorem :: ORDINAL4:7

    ( dom f1) = ( dom fi) & ( dom fi) = ( dom f2) & A is_limes_of f1 & A is_limes_of f2 & (for A st A in ( dom fi) holds (f1 . A) c= (fi . A) & (fi . A) c= (f2 . A)) implies A is_limes_of fi

    proof

      assume that

       A1: ( dom f1) = ( dom fi) and

       A2: ( dom fi) = ( dom f2) and

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

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

       A5: for A st A in ( dom fi) holds (f1 . A) c= (fi . A) & (fi . A) c= (f2 . A);

      per cases ;

        case A = 0 ;

        then

        consider B be Ordinal such that

         A6: B in ( dom f2) and

         A7: for C st B c= C & C in ( dom f2) holds (f2 . C) = {} by A4;

        take B;

        thus B in ( dom fi) by A2, A6;

        let C;

        assume that

         A8: B c= C and

         A9: C in ( dom fi);

        (f2 . C) = {} by A2, A7, A8, A9;

        hence thesis by A5, A9, XBOOLE_1: 3;

      end;

        case A <> 0 ;

        let B, C;

        assume that

         A10: B in A and

         A11: A in C;

        consider D2 be Ordinal such that

         A12: D2 in ( dom f2) and

         A13: for A1 st D2 c= A1 & A1 in ( dom f2) holds B in (f2 . A1) & (f2 . A1) in C by A4, A10, A11;

        consider D1 be Ordinal such that

         A14: D1 in ( dom f1) and

         A15: for A1 st D1 c= A1 & A1 in ( dom f1) holds B in (f1 . A1) & (f1 . A1) in C by A3, A10, A11;

        take D = (D1 \/ D2);

        thus D in ( dom fi) by A1, A2, A14, A12, ORDINAL3: 12;

        let A1;

        assume that

         A16: D c= A1 and

         A17: A1 in ( dom fi);

        reconsider B1 = (fi . A1), B2 = (f2 . A1) as Ordinal;

        

         A18: B1 c= B2 by A5, A17;

        D2 c= D by XBOOLE_1: 7;

        then D2 c= A1 by A16;

        then

         A19: B2 in C by A2, A13, A17;

        D1 c= D by XBOOLE_1: 7;

        then D1 c= A1 by A16;

        then

         A20: B in (f1 . A1) by A1, A15, A17;

        (f1 . A1) c= (fi . A1) by A5, A17;

        hence thesis by A20, A18, A19, ORDINAL1: 12;

      end;

    end;

    theorem :: ORDINAL4:8

    

     Th8: ( dom fi) <> {} & ( dom fi) is limit_ordinal & fi is increasing implies ( sup fi) is_limes_of fi & ( lim fi) = ( sup fi)

    proof

      assume that

       A1: ( dom fi) <> {} & ( dom fi) is limit_ordinal and

       A2: A in B & B in ( dom fi) implies (fi . A) in (fi . B);

      reconsider x = (fi . {} ) as Ordinal;

       {} in ( dom fi) by A1, ORDINAL3: 8;

      then

       A3: x in ( rng fi) by FUNCT_1:def 3;

      thus ( sup fi) is_limes_of fi

      proof

        per cases ;

          case ( sup fi) = 0 ;

          hence thesis by A3, ORDINAL2: 19;

        end;

          case ( sup fi) <> 0 ;

          let A, B;

          assume that

           A4: A in ( sup fi) and

           A5: ( sup fi) in B;

          consider C such that

           A6: C in ( rng fi) and

           A7: A c= C by A4, ORDINAL2: 21;

          consider x be object such that

           A8: x in ( dom fi) and

           A9: C = (fi . x) by A6, FUNCT_1:def 3;

          reconsider x as Ordinal by A8;

          take M = ( succ x);

          thus M in ( dom fi) by A1, A8, ORDINAL1: 28;

          let D;

          assume that

           A10: M c= D and

           A11: D in ( dom fi);

          reconsider E = (fi . D) as Ordinal;

          x in M by ORDINAL1: 6;

          then C in E by A2, A9, A10, A11;

          hence A in (fi . D) by A7, ORDINAL1: 12;

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

          then E in ( sup fi) by ORDINAL2: 19;

          hence thesis by A5, ORDINAL1: 10;

        end;

      end;

      hence thesis by ORDINAL2:def 10;

    end;

    theorem :: ORDINAL4:9

    

     Th9: fi is increasing & A c= B & B in ( dom fi) implies (fi . A) c= (fi . B)

    proof

      assume that

       A1: for A, B st A in B & B in ( dom fi) holds (fi . A) in (fi . B) and

       A2: A c= B and

       A3: B in ( dom fi);

      reconsider C = (fi . B) as Ordinal;

      now

        per cases ;

          suppose A = B;

          hence thesis;

        end;

          suppose A <> B;

          then A c< B by A2;

          then A in B by ORDINAL1: 11;

          then (fi . A) in C by A1, A3;

          hence thesis by ORDINAL1:def 2;

        end;

      end;

      hence thesis;

    end;

    theorem :: ORDINAL4:10

    

     Th10: fi is increasing & A in ( dom fi) implies A c= (fi . A)

    proof

      assume that

       A1: for A, B st A in B & B in ( dom fi) holds (fi . A) in (fi . B) and

       A2: A in ( dom fi) and

       A3: not A c= (fi . A);

      defpred P[ set] means $1 in ( dom fi) & not $1 c= (fi . $1);

      

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

      consider A such that

       A5: P[A] and

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

      reconsider B = (fi . A) as Ordinal;

      

       A7: B in A by A5, ORDINAL1: 16;

      then not B c= (fi . B) by A1, A5, ORDINAL1: 5;

      hence contradiction by A5, A6, A7, ORDINAL1: 10;

    end;

    theorem :: ORDINAL4:11

    

     Th11: phi is increasing implies (phi " A) is epsilon-transitive epsilon-connected set

    proof

      assume

       A1: for A, B st A in B & B in ( dom phi) holds (phi . A) in (phi . B);

      now

        let X;

        assume

         A2: X in (phi " A);

        then

         A3: X in ( dom phi) by FUNCT_1:def 7;

        hence X is Ordinal;

        reconsider B = X as Ordinal by A3;

        

         A4: (phi . X) in A by A2, FUNCT_1:def 7;

        thus X c= (phi " A)

        proof

          let x be object;

          assume

           A5: x in X;

          then x in B;

          then

          reconsider C = x, D = (phi . B) as Ordinal;

          reconsider E = (phi . C) as Ordinal;

          E in D by A1, A3, A5;

          then

           A6: (phi . x) in A by A4, ORDINAL1: 10;

          C in ( dom phi) by A3, A5, ORDINAL1: 10;

          hence thesis by A6, FUNCT_1:def 7;

        end;

      end;

      hence thesis by ORDINAL1: 19;

    end;

    theorem :: ORDINAL4:12

    

     Th12: f1 is increasing implies (f2 * f1) is Ordinal-Sequence

    proof

      

       A1: ( dom (f2 * f1)) = (f1 " ( dom f2)) by RELAT_1: 147;

      assume f1 is increasing;

      then ( dom (f2 * f1)) is Ordinal by A1, Th11;

      then

      reconsider f = (f2 * f1) as Sequence by ORDINAL1:def 7;

      consider A such that

       A2: ( rng f2) c= A by ORDINAL2:def 4;

      ( rng f) c= ( rng f2) by RELAT_1: 26;

      then ( rng f) c= A by A2;

      hence thesis by ORDINAL2:def 4;

    end;

    theorem :: ORDINAL4:13

    

     Th13: f1 is increasing & f2 is increasing implies ex phi st phi = (f1 * f2) & phi is increasing

    proof

      assume that

       A1: f1 is increasing and

       A2: f2 is increasing;

      reconsider f = (f1 * f2) as Ordinal-Sequence by A2, Th12;

      take f;

      thus f = (f1 * f2);

      let A, B;

      assume that

       A3: A in B and

       A4: B in ( dom f);

      reconsider A1 = (f2 . A), B1 = (f2 . B) as Ordinal;

      

       A5: B1 in ( dom f1) by A4, FUNCT_1: 11;

      ( dom f) c= ( dom f2) by RELAT_1: 25;

      then

       A6: A1 in B1 by A2, A3, A4;

      

       A7: (f . B) = (f1 . B1) by A4, FUNCT_1: 12;

      (f . A) = (f1 . A1) by A3, A4, FUNCT_1: 12, ORDINAL1: 10;

      hence thesis by A1, A6, A5, A7;

    end;

    theorem :: ORDINAL4:14

    

     Th14: f1 is increasing & A is_limes_of f2 & ( sup ( rng f1)) = ( dom f2) & fi = (f2 * f1) implies A is_limes_of fi

    proof

      assume that

       A1: f1 is increasing and

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

       A3: ( sup ( rng f1)) = ( dom f2) and

       A4: fi = (f2 * f1);

      per cases ;

        case A = 0 ;

        then

        consider B such that

         A5: B in ( dom f2) and

         A6: for C st B c= C & C in ( dom f2) holds (f2 . C) = {} by A2;

        consider B1 be Ordinal such that

         A7: B1 in ( rng f1) and

         A8: B c= B1 by A3, A5, ORDINAL2: 21;

        consider x be object such that

         A9: x in ( dom f1) and

         A10: B1 = (f1 . x) by A7, FUNCT_1:def 3;

        reconsider x as Ordinal by A9;

        take x;

        B1 in ( dom f2) by A3, A7, ORDINAL2: 19;

        hence x in ( dom fi) by A4, A9, A10, FUNCT_1: 11;

        let C such that

         A11: x c= C and

         A12: C in ( dom fi);

        reconsider C1 = (f1 . C) as Ordinal;

        

         A13: ( dom fi) c= ( dom f1) by A4, RELAT_1: 25;

        then B1 c= C1 by A1, A10, A11, A12, Th9;

        then

         A14: B c= C1 by A8;

        C1 in ( rng f1) by A12, A13, FUNCT_1:def 3;

        then (f2 . C1) = {} by A3, A6, A14, ORDINAL2: 19;

        hence thesis by A4, A12, FUNCT_1: 12;

      end;

        case A <> 0 ;

        let B, C;

        assume that

         A15: B in A and

         A16: A in C;

        consider D such that

         A17: D in ( dom f2) and

         A18: for A1 st D c= A1 & A1 in ( dom f2) holds B in (f2 . A1) & (f2 . A1) in C by A2, A15, A16;

        consider B1 be Ordinal such that

         A19: B1 in ( rng f1) and

         A20: D c= B1 by A3, A17, ORDINAL2: 21;

        consider x be object such that

         A21: x in ( dom f1) and

         A22: B1 = (f1 . x) by A19, FUNCT_1:def 3;

        reconsider x as Ordinal by A21;

        take x;

        B1 in ( dom f2) by A3, A19, ORDINAL2: 19;

        hence x in ( dom fi) by A4, A21, A22, FUNCT_1: 11;

        let E be Ordinal such that

         A23: x c= E and

         A24: E in ( dom fi);

        reconsider E1 = (f1 . E) as Ordinal;

        

         A25: ( dom fi) c= ( dom f1) by A4, RELAT_1: 25;

        then E1 in ( rng f1) by A24, FUNCT_1:def 3;

        then

         A26: E1 in ( dom f2) by A3, ORDINAL2: 19;

        B1 c= E1 by A1, A22, A23, A24, A25, Th9;

        then

         A27: D c= E1 by A20;

        then

         A28: (f2 . E1) in C by A18, A26;

        B in (f2 . E1) by A18, A27, A26;

        hence thesis by A4, A24, A28, FUNCT_1: 12;

      end;

    end;

    theorem :: ORDINAL4:15

    

     Th15: phi is increasing implies (phi | A) is increasing

    proof

      assume

       A1: for A, B st A in B & B in ( dom phi) holds (phi . A) in (phi . B);

      let B, C such that

       A2: B in C and

       A3: C in ( dom (phi | A));

      

       A4: (phi . B) = ((phi | A) . B) by A2, A3, FUNCT_1: 47, ORDINAL1: 10;

      ( dom (phi | A)) c= ( dom phi) by RELAT_1: 60;

      then (phi . B) in (phi . C) by A1, A2, A3;

      hence thesis by A3, A4, FUNCT_1: 47;

    end;

    theorem :: ORDINAL4:16

    

     Th16: phi is increasing & ( dom phi) is limit_ordinal implies ( sup phi) is limit_ordinal

    proof

      assume that

       A1: phi is increasing and

       A2: ( dom phi) is limit_ordinal;

      now

        let A;

        assume A in ( sup phi);

        then

        consider B such that

         A3: B in ( rng phi) and

         A4: A c= B by ORDINAL2: 21;

        consider x be object such that

         A5: x in ( dom phi) and

         A6: B = (phi . x) by A3, FUNCT_1:def 3;

        reconsider x as Ordinal by A5;

        

         A7: ( succ x) in ( dom phi) by A2, A5, ORDINAL1: 28;

        reconsider C = (phi . ( succ x)) as Ordinal;

        x in ( succ x) by ORDINAL1: 6;

        then B in C by A1, A6, A7;

        then

         A8: ( succ B) c= C by ORDINAL1: 21;

        

         A9: ( succ A) c= ( succ B) by A4, ORDINAL2: 1;

        C in ( rng phi) by A7, FUNCT_1:def 3;

        then C in ( sup phi) by ORDINAL2: 19;

        then ( succ B) in ( sup phi) by A8, ORDINAL1: 12;

        hence ( succ A) in ( sup phi) by A9, ORDINAL1: 12;

      end;

      hence thesis by ORDINAL1: 28;

    end;

    

     Lm5: ( rng f) c= X implies ((g | X) * f) = (g * f)

    proof

      

       A1: (f " ( rng f)) = ( dom f) by RELAT_1: 134;

      assume ( rng f) c= X;

      then

       A2: (f " ( rng f)) c= (f " X) by RELAT_1: 143;

      (f " X) c= ( dom f) by RELAT_1: 132;

      then

       A3: (f " X) = ( dom f) by A2, A1;

      ( dom ((g | X) * f)) = (f " ( dom (g | X))) by RELAT_1: 147

      .= (f " (( dom g) /\ X)) by RELAT_1: 61

      .= ((f " ( dom g)) /\ (f " X)) by FUNCT_1: 68

      .= (f " ( dom g)) by A3, RELAT_1: 132, XBOOLE_1: 28

      .= ( dom (g * f)) by RELAT_1: 147;

      hence thesis by GRFUNC_1: 3, RELAT_1: 64;

    end;

    theorem :: ORDINAL4:17

    fi is increasing & fi is continuous & psi is continuous & phi = (psi * fi) implies phi is continuous

    proof

      assume that

       A1: fi is increasing and

       A2: for A, B st A in ( dom fi) & A <> 0 & A is limit_ordinal & B = (fi . A) holds B is_limes_of (fi | A) and

       A3: for A, B st A in ( dom psi) & A <> 0 & A is limit_ordinal & B = (psi . A) holds B is_limes_of (psi | A) and

       A4: phi = (psi * fi);

      let A, B such that

       A5: A in ( dom phi) and

       A6: A <> 0 and

       A7: A is limit_ordinal and

       A8: B = (phi . A);

      reconsider A1 = (fi . A) as Ordinal;

      

       A9: (fi | A) is increasing by A1, Th15;

      

       A10: ( dom phi) c= ( dom fi) by A4, RELAT_1: 25;

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

      then

       A11: ( dom (fi | A)) = A by RELAT_1: 62;

      A1 is_limes_of (fi | A) by A2, A5, A6, A7, A10;

      then ( lim (fi | A)) = A1 by ORDINAL2:def 10;

      then

       A12: ( sup (fi | A)) = A1 by A6, A7, A11, A9, Th8;

      

       A13: B = (psi . A1) by A4, A5, A8, FUNCT_1: 12;

      

       A14: {} in A by A6, ORDINAL3: 8;

      

       A15: A1 in ( dom psi) by A4, A5, FUNCT_1: 11;

      then A1 c= ( dom psi) by ORDINAL1:def 2;

      then

       A16: ( dom (psi | A1)) = A1 by RELAT_1: 62;

      

       A17: ( rng (fi | A)) c= ( sup ( rng (fi | A)))

      proof

        let x be object;

        assume

         A18: x in ( rng (fi | A));

        then ex y be object st y in ( dom (fi | A)) & x = ((fi | A) . y) by FUNCT_1:def 3;

        hence thesis by A18, ORDINAL2: 19;

      end;

      (phi | A) = (psi * (fi | A)) by A4, RELAT_1: 83;

      then

       A19: (phi | A) = ((psi | A1) * (fi | A)) by A17, A12, Lm5;

      A c= A1 by A1, A5, A10, Th10;

      then B is_limes_of (psi | A1) by A3, A7, A13, A15, A11, A14, A9, A12, Th16;

      hence thesis by A9, A16, A12, A19, Th14;

    end;

    theorem :: ORDINAL4:18

    (for A st A in ( dom fi) holds (fi . A) = (C +^ A)) implies fi is increasing

    proof

      assume

       A1: for A st A in ( dom fi) holds (fi . A) = (C +^ A);

      let A, B;

      assume that

       A2: A in B and

       A3: B in ( dom fi);

      

       A4: (fi . B) = (C +^ B) by A1, A3;

      (fi . A) = (C +^ A) by A1, A2, A3, ORDINAL1: 10;

      hence thesis by A2, A4, ORDINAL2: 32;

    end;

    theorem :: ORDINAL4:19

    

     Th19: C <> {} & (for A st A in ( dom fi) holds (fi . A) = (A *^ C)) implies fi is increasing

    proof

      assume that

       A1: C <> {} and

       A2: for A st A in ( dom fi) holds (fi . A) = (A *^ C);

      let A, B;

      assume that

       A3: A in B and

       A4: B in ( dom fi);

      

       A5: (fi . B) = (B *^ C) by A2, A4;

      (fi . A) = (A *^ C) by A2, A3, A4, ORDINAL1: 10;

      hence thesis by A1, A3, A5, ORDINAL2: 40;

    end;

    theorem :: ORDINAL4:20

    

     Th20: A <> {} implies ( exp ( {} ,A)) = {}

    proof

      defpred FF[ Ordinal] means $1 <> {} implies ( exp ( {} ,$1)) = {} ;

      

       A1: FF[B] implies FF[( succ B)]

      proof

        assume that FF[B] and ( succ B) <> {} ;

        

        thus ( exp ( {} ,( succ B))) = ( {} *^ ( exp ( {} ,B))) by ORDINAL2: 44

        .= {} by ORDINAL2: 35;

      end;

      

       A2: for B st B <> 0 & B is limit_ordinal & for C st C in B holds FF[C] holds FF[B]

      proof

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

        let A such that

         A3: A <> 0 and

         A4: A is limit_ordinal and

         A5: for C st C in A holds FF[C] and A <> {} ;

        consider fi such that

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

         0 is_limes_of fi

        proof

          per cases ;

            case 0 = 0 ;

            take B = 1;

             {} in A by A3, ORDINAL3: 8;

            hence B in ( dom fi) by A4, A6, Lm3, ORDINAL1: 28;

            let D;

            assume

             A7: B c= D;

            assume

             A8: D in ( dom fi);

            then FF[D] by A5, A6;

            hence thesis by A6, A7, A8, Lm3, ORDINAL1: 21;

          end;

            case 0 <> 0 ;

            thus thesis;

          end;

        end;

        then ( lim fi) = {} by ORDINAL2:def 10;

        hence thesis by A3, A4, A6, ORDINAL2: 45;

      end;

      

       A9: FF[ 0 ];

       FF[B] from ORDINAL2:sch 1( A9, A1, A2);

      hence thesis;

    end;

    

     Lm6: A <> {} & A is limit_ordinal implies for fi st ( dom fi) = A & for B st B in A holds (fi . B) = ( exp ( {} ,B)) holds 0 is_limes_of fi

    proof

      assume that

       A1: A <> {} and

       A2: A is limit_ordinal;

      let fi;

      assume that

       A3: ( dom fi) = A and

       A4: for B st B in A holds (fi . B) = ( exp ( {} ,B));

      per cases ;

        case 0 = 0 ;

        take B = 1;

         {} in A by A1, ORDINAL3: 8;

        hence B in ( dom fi) by A2, A3, Lm3, ORDINAL1: 28;

        let D;

        assume that

         A5: B c= D and

         A6: D in ( dom fi);

        

         A7: D <> {} by A5, Lm3, ORDINAL1: 21;

        ( exp ( {} ,D)) = (fi . D) by A3, A4, A6;

        hence thesis by A7, Th20;

      end;

        case 0 <> 0 ;

        thus thesis;

      end;

    end;

    

     Lm7: A <> {} implies for fi st ( dom fi) = A & for B st B in A holds (fi . B) = ( exp (1,B)) holds 1 is_limes_of fi

    proof

      assume that

       A1: A <> {} ;

      let fi;

      assume that

       A2: ( dom fi) = A and

       A3: for B st B in A holds (fi . B) = ( exp (1,B));

      per cases ;

        case 1 = 0 ;

        hence thesis;

      end;

        case 1 <> 0 ;

        let A1,A2 be Ordinal such that

         A4: A1 in 1 and

         A5: 1 in A2;

        take B = {} ;

        thus B in ( dom fi) by A1, A2, ORDINAL3: 8;

        let D;

        assume that B c= D and

         A6: D in ( dom fi);

        ( exp (1,D)) = (fi . D) by A2, A3, A6;

        hence thesis by A4, A5, ORDINAL2: 46;

      end;

    end;

    

     Lm8: for A st A <> {} & A is limit_ordinal holds ex fi st ( dom fi) = A & (for B st B in A holds (fi . B) = ( exp (C,B))) & ex D st D is_limes_of fi

    proof

      defpred P[ Ordinal] means $1 <> {} & $1 is limit_ordinal & for fi st ( dom fi) = $1 & for B st B in $1 holds (fi . B) = ( exp (C,B)) holds for D holds not D is_limes_of fi;

      let A such that

       A1: A <> {} and

       A2: A is limit_ordinal and

       A3: for fi st ( dom fi) = A & for B st B in A holds (fi . B) = ( exp (C,B)) holds for D holds not D is_limes_of fi;

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

      

       A4: ex A st P[A] by A1, A2, A3;

      consider A such that

       A5: P[A] and

       A6: for A1 st P[A1] holds A c= A1 from ORDINAL1:sch 1( A4);

      consider fi such that

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

      

       A8: C <> {} & C <> 1 by A5, A7, Lm6, Lm7;

      then {} in C by ORDINAL3: 8;

      then 1 c= C by Lm3, ORDINAL1: 21;

      then

       A9: 1 c< C by A8;

      

       A10: for B2,B1 be Ordinal st B1 in B2 & B2 in A holds ( exp (C,B1)) in ( exp (C,B2))

      proof

        defpred V[ Ordinal] means for B1 be Ordinal st B1 in $1 & $1 in A holds ( exp (C,B1)) in ( exp (C,$1));

        

         A11: V[B] implies V[( succ B)]

        proof

          assume

           A12: for B1 be Ordinal st B1 in B & B in A holds ( exp (C,B1)) in ( exp (C,B));

          let B1 be Ordinal such that

           A13: B1 in ( succ B) and

           A14: ( succ B) in A;

          

           A15: B1 c= B by A13, ORDINAL1: 22;

          B in ( succ B) by ORDINAL1: 6;

          then

           A16: B in A by A14, ORDINAL1: 10;

          

           A17: (1 *^ ( exp (C,B))) = ( exp (C,B)) by ORDINAL2: 39;

          

           A18: ( exp (C,B)) <> {}

          proof

            now

              per cases ;

                suppose B = {} ;

                hence thesis by ORDINAL2: 43;

              end;

                suppose

                 A19: B <> {} ;

                B in ( succ B) by ORDINAL1: 6;

                then B in A by A14, ORDINAL1: 10;

                hence thesis by A12, A19, ORDINAL3: 8;

              end;

            end;

            hence thesis;

          end;

          

           A20: ( exp (C,( succ B))) = (C *^ ( exp (C,B))) by ORDINAL2: 44;

          then

           A21: ( exp (C,B)) in ( exp (C,( succ B))) by A9, A18, A17, ORDINAL1: 11, ORDINAL2: 40;

          now

            assume B1 <> B;

            then B1 c< B by A15;

            then B1 in B by ORDINAL1: 11;

            then ( exp (C,B1)) in ( exp (C,B)) by A12, A16;

            hence thesis by A21, ORDINAL1: 10;

          end;

          hence thesis by A9, A18, A20, A17, ORDINAL1: 11, ORDINAL2: 40;

        end;

        

         A22: for B st B <> 0 & B is limit_ordinal & for D st D in B holds V[D] holds V[B]

        proof

          let B such that

           A23: B <> 0 and

           A24: B is limit_ordinal and

           A25: for D st D in B holds V[D];

          let B1 be Ordinal;

          assume that

           A26: B1 in B and

           A27: B in A;

          consider psi such that

           A28: ( dom psi) = B and

           A29: for D st D in B holds (psi . D) = ( exp (C,D)) and ex D st D is_limes_of psi by A6, A24, A26, A27, ORDINAL1: 5;

          (psi . B1) = ( exp (C,B1)) by A26, A29;

          then

           A30: ( exp (C,B1)) in ( rng psi) by A26, A28, FUNCT_1:def 3;

          psi is increasing

          proof

            let B1,B2 be Ordinal;

            assume that

             A31: B1 in B2 and

             A32: B2 in ( dom psi);

            B2 in A by A27, A28, A32, ORDINAL1: 10;

            then

             A33: ( exp (C,B1)) in ( exp (C,B2)) by A25, A28, A31, A32;

            (psi . B1) = ( exp (C,B1)) by A28, A29, A31, A32, ORDINAL1: 10;

            hence thesis by A28, A29, A32, A33;

          end;

          then

           A34: ( lim psi) = ( sup psi) by A23, A24, A28, Th8;

          ( exp (C,B)) = ( lim psi) by A23, A24, A28, A29, ORDINAL2: 45;

          hence thesis by A34, A30, ORDINAL2: 19;

        end;

        

         A35: V[ 0 ];

        thus for B holds V[B] from ORDINAL2:sch 1( A35, A11, A22);

      end;

      fi is increasing

      proof

        let B1,B2 be Ordinal;

        assume that

         A36: B1 in B2 and

         A37: B2 in ( dom fi);

        

         A38: (fi . B1) = ( exp (C,B1)) by A7, A36, A37, ORDINAL1: 10;

        ( exp (C,B1)) in ( exp (C,B2)) by A7, A10, A36, A37;

        hence thesis by A7, A37, A38;

      end;

      then ( sup fi) is_limes_of fi by A5, A7, Th8;

      hence contradiction by A5, A7;

    end;

    theorem :: ORDINAL4:21

    

     Th21: A <> {} & A is limit_ordinal implies for fi st ( dom fi) = A & for B st B in A holds (fi . B) = ( exp (C,B)) holds ( exp (C,A)) is_limes_of fi

    proof

      assume that

       A1: A <> {} and

       A2: A is limit_ordinal;

      consider psi such that

       A3: ( dom psi) = A and

       A4: for B st B in A holds (psi . B) = ( exp (C,B)) and

       A5: ex D st D is_limes_of psi by A1, A2, Lm8;

      let fi such that

       A6: ( dom fi) = A and

       A7: for B st B in A holds (fi . B) = ( exp (C,B));

      now

        let x be object;

        assume

         A8: x in A;

        then

        reconsider B = x as Ordinal;

        

        thus (fi . x) = ( exp (C,B)) by A7, A8

        .= (psi . x) by A4, A8;

      end;

      then fi = psi by A6, A3, FUNCT_1: 2;

      then

      consider D such that

       A9: D is_limes_of fi by A5;

      D = ( lim fi) by A9, ORDINAL2:def 10

      .= ( exp (C,A)) by A1, A2, A6, A7, ORDINAL2: 45;

      hence thesis by A9;

    end;

    theorem :: ORDINAL4:22

    

     Th22: C <> {} implies ( exp (C,A)) <> {}

    proof

      defpred P[ Ordinal] means ( exp (C,$1)) <> {} ;

      assume

       A1: C <> {} ;

      

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

      proof

        let A such that

         A3: ( exp (C,A)) <> {} ;

        ( exp (C,( succ A))) = (C *^ ( exp (C,A))) by ORDINAL2: 44;

        hence thesis by A1, A3, ORDINAL3: 31;

      end;

      

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

      proof

        let A such that

         A5: A <> 0 and

         A6: A is limit_ordinal and

         A7: for B st B in A holds ( exp (C,B)) <> {} ;

        consider fi such that

         A8: ( dom fi) = A and

         A9: for B st B in A holds (fi . B) = ( exp (C,B)) and

         A10: ex D st D is_limes_of fi by A5, A6, Lm8;

        

         A11: ( exp (C,A)) = ( lim fi) by A5, A6, A8, A9, ORDINAL2: 45;

        assume

         A12: ( exp (C,A)) = {} ;

        consider D such that

         A13: D is_limes_of fi by A10;

        ( lim fi) = D by A13, ORDINAL2:def 10;

        then

        consider B such that

         A14: B in ( dom fi) and

         A15: for D st B c= D & D in ( dom fi) holds (fi . D) = {} by A11, A13, A12, ORDINAL2:def 9;

        (fi . B) = ( exp (C,B)) by A8, A9, A14;

        hence contradiction by A7, A8, A14, A15;

      end;

      

       A16: P[ 0 ] by ORDINAL2: 43;

      for A holds P[A] from ORDINAL2:sch 1( A16, A2, A4);

      hence thesis;

    end;

    theorem :: ORDINAL4:23

    

     Th23: 1 in C implies ( exp (C,A)) in ( exp (C,( succ A)))

    proof

      

       A1: (1 *^ ( exp (C,A))) = ( exp (C,A)) by ORDINAL2: 39;

      assume 1 in C;

      then ( exp (C,A)) in (C *^ ( exp (C,A))) by A1, Th22, ORDINAL2: 40;

      hence thesis by ORDINAL2: 44;

    end;

    theorem :: ORDINAL4:24

    

     Th24: 1 in C & A in B implies ( exp (C,A)) in ( exp (C,B))

    proof

      defpred OO[ Ordinal] means for A st A in $1 holds ( exp (C,A)) in ( exp (C,$1));

      

       A1: for B st B <> 0 & B is limit_ordinal & for D st D in B holds OO[D] holds OO[B]

      proof

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

        let B such that

         A2: B <> 0 and

         A3: B is limit_ordinal and

         A4: for D st D in B holds OO[D];

        consider fi such that

         A5: ( dom fi) = B & for D st D in B holds (fi . D) = F(D) from ORDINAL2:sch 3;

        fi is increasing

        proof

          let B1,B2 be Ordinal;

          assume that

           A6: B1 in B2 and

           A7: B2 in ( dom fi);

          

           A8: (fi . B1) = ( exp (C,B1)) by A5, A6, A7, ORDINAL1: 10;

          ( exp (C,B1)) in ( exp (C,B2)) by A4, A5, A6, A7;

          hence thesis by A5, A7, A8;

        end;

        then

         A9: ( sup fi) = ( lim fi) by A2, A3, A5, Th8;

        let A such that

         A10: A in B;

        (fi . A) = ( exp (C,A)) by A10, A5;

        then

         A11: ( exp (C,A)) in ( rng fi) by A10, A5, FUNCT_1:def 3;

        ( exp (C,B)) = ( lim fi) by A2, A3, A5, ORDINAL2: 45;

        hence thesis by A9, A11, ORDINAL2: 19;

      end;

      assume

       A12: 1 in C;

      

       A13: for B st OO[B] holds OO[( succ B)]

      proof

        let B such that

         A14: for A st A in B holds ( exp (C,A)) in ( exp (C,B));

        let A;

        assume A in ( succ B);

        then

         A15: A c= B by ORDINAL1: 22;

         A16:

        now

          assume A <> B;

          then A c< B by A15;

          hence ( exp (C,A)) in ( exp (C,B)) by A14, ORDINAL1: 11;

        end;

        ( exp (C,B)) in ( exp (C,( succ B))) by A12, Th23;

        hence thesis by A16, ORDINAL1: 10;

      end;

      

       A17: OO[ 0 ];

      for B holds OO[B] from ORDINAL2:sch 1( A17, A13, A1);

      hence thesis;

    end;

    theorem :: ORDINAL4:25

    

     Th25: 1 in C & (for A st A in ( dom fi) holds (fi . A) = ( exp (C,A))) implies fi is increasing

    proof

      assume that

       A1: 1 in C and

       A2: for A st A in ( dom fi) holds (fi . A) = ( exp (C,A));

      let A, B;

      assume that

       A3: A in B and

       A4: B in ( dom fi);

      

       A5: (fi . B) = ( exp (C,B)) by A2, A4;

      (fi . A) = ( exp (C,A)) by A2, A3, A4, ORDINAL1: 10;

      hence thesis by A1, A3, A5, Th24;

    end;

    theorem :: ORDINAL4:26

    1 in C & A <> {} & A is limit_ordinal implies for fi st ( dom fi) = A & for B st B in A holds (fi . B) = ( exp (C,B)) holds ( exp (C,A)) = ( sup fi)

    proof

      assume that

       A1: 1 in C and

       A2: A <> {} and

       A3: A is limit_ordinal;

      let fi;

      assume that

       A4: ( dom fi) = A and

       A5: for B st B in A holds (fi . B) = ( exp (C,B));

      fi is increasing by A1, A4, A5, Th25;

      then ( lim fi) = ( sup fi) by A2, A3, A4, Th8;

      hence thesis by A2, A3, A4, A5, ORDINAL2: 45;

    end;

    theorem :: ORDINAL4:27

    C <> {} & A c= B implies ( exp (C,A)) c= ( exp (C,B))

    proof

      

       A1: A c< B iff A c= B & A <> B;

      assume C <> {} ;

      then {} in C by ORDINAL3: 8;

      then

       A2: 1 c= C by Lm3, ORDINAL1: 21;

      assume A c= B;

      then

       A3: A in B or A = B by A1, ORDINAL1: 11;

      now

        per cases ;

          suppose

           A4: C = 1;

          then ( exp (C,A)) = 1 by ORDINAL2: 46;

          hence thesis by A4, ORDINAL2: 46;

        end;

          suppose C <> 1;

          then 1 c< C by A2;

          then 1 in C by ORDINAL1: 11;

          then ( exp (C,A)) in ( exp (C,B)) or ( exp (C,A)) = ( exp (C,B)) by A3, Th24;

          hence thesis by ORDINAL1:def 2;

        end;

      end;

      hence thesis;

    end;

    theorem :: ORDINAL4:28

    A c= B implies ( exp (A,C)) c= ( exp (B,C))

    proof

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

      assume

       A1: A c= B;

      

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

      proof

        let C;

        

         A3: ( exp (B,( succ C))) = (B *^ ( exp (B,C))) by ORDINAL2: 44;

        ( exp (A,( succ C))) = (A *^ ( exp (A,C))) by ORDINAL2: 44;

        hence thesis by A1, A3, ORDINAL3: 20;

      end;

      

       A4: for C st C <> 0 & C is limit_ordinal & for D st D in C holds P[D] holds P[C]

      proof

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

        let C;

        assume that

         A5: C <> 0 and

         A6: C is limit_ordinal and

         A7: for D st D in C holds ( exp (A,D)) c= ( exp (B,D));

        consider f1 such that

         A8: ( dom f1) = C & for D st D in C holds (f1 . D) = F(D) from ORDINAL2:sch 3;

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

        consider f2 such that

         A9: ( dom f2) = C & for D st D in C holds (f2 . D) = F(D) from ORDINAL2:sch 3;

         A10:

        now

          let D;

          assume

           A11: D in ( dom f1);

          then

           A12: (f1 . D) = ( exp (A,D)) by A8;

          (f2 . D) = ( exp (B,D)) by A8, A9, A11;

          hence (f1 . D) c= (f2 . D) by A7, A8, A11, A12;

        end;

        

         A13: ( exp (A,C)) is_limes_of f1 by A5, A6, A8, Th21;

        ( exp (B,C)) is_limes_of f2 by A5, A6, A9, Th21;

        hence thesis by A8, A9, A13, A10, Th6;

      end;

      ( exp (A, {} )) = 1 by ORDINAL2: 43;

      then

       A14: P[ 0 ] by ORDINAL2: 43;

      for C holds P[C] from ORDINAL2:sch 1( A14, A2, A4);

      hence thesis;

    end;

    theorem :: ORDINAL4:29

    1 in C & A <> {} implies 1 in ( exp (C,A))

    proof

      assume that

       A1: 1 in C and

       A2: A <> {} ;

      ( exp (C, {} )) = 1 by ORDINAL2: 43;

      hence thesis by A1, A2, Th24, ORDINAL3: 8;

    end;

    theorem :: ORDINAL4:30

    

     Th30: ( exp (C,(A +^ B))) = (( exp (C,B)) *^ ( exp (C,A)))

    proof

      defpred P[ Ordinal] means ( exp (C,(A +^ $1))) = (( exp (C,$1)) *^ ( exp (C,A)));

      

       A1: 1 = ( exp (C, {} )) by ORDINAL2: 43;

      

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

      proof

        let B such that

         A3: ( exp (C,(A +^ B))) = (( exp (C,B)) *^ ( exp (C,A)));

        

        thus ( exp (C,(A +^ ( succ B)))) = ( exp (C,( succ (A +^ B)))) by ORDINAL2: 28

        .= (C *^ ( exp (C,(A +^ B)))) by ORDINAL2: 44

        .= ((C *^ ( exp (C,B))) *^ ( exp (C,A))) by A3, ORDINAL3: 50

        .= (( exp (C,( succ B))) *^ ( exp (C,A))) by ORDINAL2: 44;

      end;

      

       A4: for B st B <> 0 & B is limit_ordinal & for D st D in B holds P[D] holds P[B]

      proof

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

        let B such that

         A5: B <> 0 and

         A6: B is limit_ordinal and

         A7: for D st D in B holds ( exp (C,(A +^ D))) = (( exp (C,D)) *^ ( exp (C,A)));

        consider fi such that

         A8: ( dom fi) = B & for D st D in B holds (fi . D) = F(D) from ORDINAL2:sch 3;

        consider psi such that

         A9: ( dom psi) = (A +^ B) & for D st D in (A +^ B) holds (psi . D) = F(D) from ORDINAL2:sch 3;

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

        consider f1 such that

         A10: ( dom f1) = A & for D st D in A holds (f1 . D) = F(D) from ORDINAL2:sch 3;

         A11:

        now

          let D;

          assume D in ( dom (fi *^ ( exp (C,A))));

          then

           A12: D in ( dom fi) by ORDINAL3:def 4;

          

          hence (psi . (( dom f1) +^ D)) = ( exp (C,(A +^ D))) by A8, A9, A10, ORDINAL2: 32

          .= (( exp (C,D)) *^ ( exp (C,A))) by A7, A8, A12

          .= ((fi . D) *^ ( exp (C,A))) by A8, A12

          .= ((fi *^ ( exp (C,A))) . D) by A12, ORDINAL3:def 4;

        end;

         A13:

        now

          let D such that

           A14: D in ( dom f1);

          A c= (A +^ B) by ORDINAL3: 24;

          

          hence (psi . D) = ( exp (C,D)) by A9, A10, A14

          .= (f1 . D) by A10, A14;

        end;

        ( dom psi) = (( dom f1) +^ ( dom (fi *^ ( exp (C,A))))) by A8, A9, A10, ORDINAL3:def 4;

        then

         A15: psi = (f1 ^ (fi *^ ( exp (C,A)))) by A13, A11, Def1;

        (( exp (C,B)) *^ ( exp (C,A))) is_limes_of (fi *^ ( exp (C,A))) by A5, A6, A8, Th5, Th21;

        then

         A16: (( exp (C,B)) *^ ( exp (C,A))) is_limes_of psi by A15, Th3;

        

         A17: (A +^ B) <> {} by A5, ORDINAL3: 26;

        (A +^ B) is limit_ordinal by A5, A6, ORDINAL3: 29;

        then ( lim psi) = ( exp (C,(A +^ B))) by A9, A17, ORDINAL2: 45;

        hence thesis by A16, ORDINAL2:def 10;

      end;

      ( exp (C,A)) = (1 *^ ( exp (C,A))) by ORDINAL2: 39;

      then

       A18: P[ 0 ] by A1, ORDINAL2: 27;

      for B holds P[B] from ORDINAL2:sch 1( A18, A2, A4);

      hence thesis;

    end;

    theorem :: ORDINAL4:31

    ( exp (( exp (C,A)),B)) = ( exp (C,(B *^ A)))

    proof

      defpred P[ Ordinal] means ( exp (( exp (C,A)),$1)) = ( exp (C,($1 *^ A)));

      

       A1: ( exp (C, {} )) = 1 by ORDINAL2: 43;

      

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

      proof

        let B;

        assume ( exp (( exp (C,A)),B)) = ( exp (C,(B *^ A)));

        

        hence ( exp (( exp (C,A)),( succ B))) = (( exp (C,A)) *^ ( exp (C,(B *^ A)))) by ORDINAL2: 44

        .= ( exp (C,((B *^ A) +^ A))) by Th30

        .= ( exp (C,(( succ B) *^ A))) by ORDINAL2: 36;

      end;

      

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

      proof

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

        let B;

        assume that

         A4: B <> 0 and

         A5: B is limit_ordinal and

         A6: for D st D in B holds ( exp (( exp (C,A)),D)) = ( exp (C,(D *^ A)));

        consider fi such that

         A7: ( dom fi) = B & for D st D in B holds (fi . D) = F(D) from ORDINAL2:sch 3;

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

        consider f1 such that

         A8: ( dom f1) = B & for D st D in B holds (f1 . D) = F(D) from ORDINAL2:sch 3;

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

        consider f2 such that

         A9: ( dom f2) = (B *^ A) & for D st D in (B *^ A) holds (f2 . D) = F(D) from ORDINAL2:sch 3;

         A10:

        now

          assume

           A11: A <> {} ;

          then (B *^ A) <> {} by A4, ORDINAL3: 31;

          then

           A12: ( exp (C,(B *^ A))) is_limes_of f2 by A5, A9, Th21, ORDINAL3: 40;

          

           A13: ( rng f1) c= ( dom f2)

          proof

            let x be object;

            assume x in ( rng f1);

            then

            consider y be object such that

             A14: y in ( dom f1) and

             A15: x = (f1 . y) by FUNCT_1:def 3;

            reconsider y as Ordinal by A14;

            x = (y *^ A) by A8, A14, A15;

            hence thesis by A8, A9, A11, A14, ORDINAL2: 40;

          end;

          

           A16: ( sup ( rng f1)) = ( dom f2)

          proof

            ( sup ( rng f1)) c= ( sup ( dom f2)) by A13, ORDINAL2: 22;

            hence ( sup ( rng f1)) c= ( dom f2) by ORDINAL2: 18;

            let x be object;

            assume

             A17: x in ( dom f2);

            then

            reconsider D = x as Ordinal;

            consider A1 such that

             A18: A1 in B and

             A19: D in (A1 *^ A) by A5, A9, A17, ORDINAL3: 41;

            (f1 . A1) = (A1 *^ A) by A8, A18;

            then (A1 *^ A) in ( rng f1) by A8, A18, FUNCT_1:def 3;

            then (A1 *^ A) in ( sup ( rng f1)) by ORDINAL2: 19;

            hence thesis by A19, ORDINAL1: 10;

          end;

          

           A20: ( dom (f2 * f1)) = B

          proof

            thus ( dom (f2 * f1)) c= B by A8, RELAT_1: 25;

            let x be object;

            assume

             A21: x in B;

            then

            reconsider E = x as Ordinal;

            

             A22: (f1 . E) = (E *^ A) by A8, A21;

            (E *^ A) in (B *^ A) by A11, A21, ORDINAL2: 40;

            hence thesis by A8, A9, A21, A22, FUNCT_1: 11;

          end;

          now

            let x be object;

            assume

             A23: x in B;

            then

            reconsider D = x as Ordinal;

            

             A24: (f1 . D) = (D *^ A) by A8, A23;

            

            thus (fi . x) = ( exp (( exp (C,A)),D)) by A7, A23

            .= ( exp (C,(D *^ A))) by A6, A23

            .= (f2 . (f1 . D)) by A9, A11, A23, A24, ORDINAL2: 40

            .= ((f2 * f1) . x) by A8, A23, FUNCT_1: 13;

          end;

          then fi = (f2 * f1) by A7, A20, FUNCT_1: 2;

          then ( exp (C,(B *^ A))) is_limes_of fi by A8, A11, A12, A16, Th14, Th19;

          then ( exp (C,(B *^ A))) = ( lim fi) by ORDINAL2:def 10;

          hence thesis by A4, A5, A7, ORDINAL2: 45;

        end;

        

         A25: (B *^ {} ) = {} by ORDINAL2: 38;

        ( exp (C, {} )) = 1 by ORDINAL2: 43;

        hence thesis by A25, A10, ORDINAL2: 46;

      end;

      ( exp (( exp (C,A)), {} )) = 1 by ORDINAL2: 43;

      then

       A26: P[ 0 ] by A1, ORDINAL2: 35;

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

      hence thesis;

    end;

    theorem :: ORDINAL4:32

    1 in C implies A c= ( exp (C,A))

    proof

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

      assume

       A1: 1 in C;

      

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

      proof

        assume

         A3: B c= ( exp (C,B));

        

         A4: ( exp (C,B)) = (1 *^ ( exp (C,B))) by ORDINAL2: 39;

        ( exp (C,( succ B))) = (C *^ ( exp (C,B))) by ORDINAL2: 44;

        then ( exp (C,B)) in ( exp (C,( succ B))) by A1, A4, Th22, ORDINAL2: 40;

        then B in ( exp (C,( succ B))) by A3, ORDINAL1: 12;

        hence thesis by ORDINAL1: 21;

      end;

      

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

      proof

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

        let A such that

         A6: A <> 0 and

         A7: A is limit_ordinal and

         A8: for B st B in A holds B c= ( exp (C,B));

        consider fi such that

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

        let x be object;

        assume

         A10: x in A;

        then

        reconsider B = x as Ordinal;

        (fi . B) = ( exp (C,B)) by A9, A10;

        then ( exp (C,B)) in ( rng fi) by A9, A10, FUNCT_1:def 3;

        then

         A11: ( exp (C,B)) in ( sup fi) by ORDINAL2: 19;

        fi is increasing by A1, A9, Th25;

        

        then

         A12: ( sup fi) = ( lim fi) by A6, A7, A9, Th8

        .= ( exp (C,A)) by A6, A7, A9, ORDINAL2: 45;

        B c= ( exp (C,B)) by A8, A10;

        hence thesis by A12, A11, ORDINAL1: 12;

      end;

      

       A13: P[ 0 ] by XBOOLE_1: 2;

       P[B] from ORDINAL2:sch 1( A13, A2, A5);

      hence thesis;

    end;

    ::$Notion-Name

    scheme :: ORDINAL4:sch1

    CriticalNumber { phi( Ordinal) -> Ordinal } :

ex A st phi(A) = A

      provided

       A1: for A, B st A in B holds phi(A) in phi(B)

       and

       A2: for A st A <> {} & A is limit_ordinal holds for phi st ( dom phi) = A & for B st B in A holds (phi . B) = phi(B) holds phi(A) is_limes_of phi;

       A3:

      now

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

        assume

         A4: ex A st P[A];

        consider A such that

         A5: P[A] and

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

        phi(phi) in phi(A) by A1, A5, ORDINAL1: 16;

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

        hence contradiction by A5, A6;

      end;

      deffunc G( Ordinal, Sequence) = {} ;

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

      consider phi such that

       A7: ( dom phi) = omega and

       A8: 0 in omega implies (phi . 0 ) = phi(0) and

       A9: 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;

      assume

       A10: not thesis;

       A11:

      now

        let A;

        

         A12: A <> phi(A) by A10;

        A c= phi(A) by A3;

        then A c< phi(A) by A12;

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

      end;

      

       A13: phi is increasing

      proof

        let A, B;

        assume that

         A14: A in B and

         A15: B in ( dom phi);

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

        

         A16: for B st B <> 0 & B is limit_ordinal & for C st C in B holds R[C] holds R[B]

        proof

          let B such that

           A17: B <> 0 and

           A18: B is limit_ordinal and for C st C in B holds (A +^ C) in omega & C <> {} implies (phi . A) in (phi . (A +^ C)) and

           A19: (A +^ B) in omega and

           A20: B <> {} ;

          (A +^ B) <> {} by A20, ORDINAL3: 26;

          then

           A21: {} in (A +^ B) by ORDINAL3: 8;

          (A +^ B) is limit_ordinal by A17, A18, ORDINAL3: 29;

          then omega c= (A +^ B) by A21, ORDINAL1:def 11;

          hence thesis by A19, ORDINAL1: 5;

        end;

        

         A22: for C st R[C] holds R[( succ C)]

        proof

          let C such that

           A23: (A +^ C) in omega & C <> {} implies (phi . A) in (phi . (A +^ C)) and

           A24: (A +^ ( succ C)) in omega and ( succ C) <> {} ;

          reconsider D = (phi . (A +^ C)) as Ordinal;

          

           A25: (A +^ C) in ( succ (A +^ C)) by ORDINAL1: 6;

          

           A26: D in phi(D) by A11;

          

           A27: (A +^ ( succ C)) = ( succ (A +^ C)) by ORDINAL2: 28;

          then (phi . (A +^ ( succ C))) = phi(D) by A9, A24;

          hence thesis by A23, A24, A25, A27, A26, ORDINAL1: 10, ORDINAL2: 27;

        end;

        

         A28: R[ 0 ];

        

         A29: for C holds R[C] from ORDINAL2:sch 1( A28, A22, A16);

        ex C st B = (A +^ C) & C <> {} by A14, ORDINAL3: 28;

        hence thesis by A7, A15, A29;

      end;

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

      consider fi such that

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

       phi({}) in ( rng phi) by A7, A8, Lm1, FUNCT_1:def 3;

      then

       A31: ( sup phi) <> {} by ORDINAL2: 19;

      then

       A32: phi(sup) is_limes_of fi by A2, A7, A13, A30, Lm2, Th16;

      

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

      proof

        let x be object;

        assume

         A34: x in ( sup fi);

        then

        reconsider A = x as Ordinal;

        consider B such that

         A35: B in ( rng fi) and

         A36: A c= B by A34, ORDINAL2: 21;

        consider y be object such that

         A37: y in ( dom fi) and

         A38: B = (fi . y) by A35, FUNCT_1:def 3;

        reconsider y as Ordinal by A37;

        consider C such that

         A39: C in ( rng phi) and

         A40: y c= C by A30, A37, ORDINAL2: 21;

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

        then

         A41: phi(y) in phi(C) or y = C by A1, A40, ORDINAL1: 11;

        B = phi(y) by A30, A37, A38;

        then

         A42: B c= phi(C) by A41, ORDINAL1:def 2;

        consider z be object such that

         A43: z in ( dom phi) and

         A44: C = (phi . z) by A39, FUNCT_1:def 3;

        reconsider z as Ordinal by A43;

        

         A45: ( succ z) in omega by A7, A43, Lm2, ORDINAL1: 28;

        then

         A46: (phi . ( succ z)) in ( rng phi) by A7, FUNCT_1:def 3;

        (phi . ( succ z)) = phi(C) by A9, A44, A45;

        then phi(C) in ( sup phi) by A46, ORDINAL2: 19;

        then B in ( sup phi) by A42, ORDINAL1: 12;

        hence thesis by A36, ORDINAL1: 12;

      end;

      

       A47: fi is increasing

      proof

        let A, B;

        assume that

         A48: A in B and

         A49: B in ( dom fi);

        

         A50: (fi . B) = phi(B) by A30, A49;

        (fi . A) = phi(A) by A30, A48, A49, ORDINAL1: 10;

        hence thesis by A1, A48, A50;

      end;

      ( sup phi) is limit_ordinal by A7, A13, Lm2, Th16;

      

      then ( sup fi) = ( lim fi) by A30, A31, A47, Th8

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

      hence contradiction by A11, A33, ORDINAL1: 5;

    end;

    reserve W for Universe;

    registration

      let W;

      cluster ordinal for Element of W;

      existence

      proof

        

         A1: ( On W) c= W by ORDINAL2: 7;

         {} in ( On W) by CLASSES2: 51, ORDINAL3: 8;

        hence thesis by A1;

      end;

    end

    definition

      let W;

      mode Ordinal of W is ordinal Element of W;

      mode Ordinal-Sequence of W is Function of ( On W), ( On W);

    end

    

     Lm9: 0 = {} ;

    registration

      let W;

      cluster non empty for Ordinal of W;

      existence

      proof

        

         A1: ( On W) c= W by ORDINAL2: 7;

         {} in ( On W) by CLASSES2: 51, ORDINAL3: 8;

        then 1 in W by A1, Lm3, CLASSES2: 5;

        hence thesis by Lm9;

      end;

    end

    registration

      let W;

      cluster ( On W) -> non empty;

      coherence by CLASSES2: 51;

    end

    registration

      let W;

      cluster -> Sequence-like Ordinal-yielding for Ordinal-Sequence of W;

      coherence

      proof

        let s be Ordinal-Sequence of W;

        thus ( dom s) is epsilon-transitive epsilon-connected by FUNCT_2:def 1;

        take ( On W);

        thus ( rng s) c= ( On W) by RELAT_1:def 19;

      end;

    end

    reserve A1,B1 for Ordinal of W,

phi for Ordinal-Sequence of W;

    scheme :: ORDINAL4:sch2

    UOSLambda { W() -> Universe , F( set) -> Ordinal of W() } :

ex phi be Ordinal-Sequence of W() st for a be Ordinal of W() holds (phi . a) = F(a);

      consider psi such that

       A1: ( dom psi) = ( On W()) & for A st A in ( On W()) holds (psi . A) = F(A) from ORDINAL2:sch 3;

      ( rng psi) c= ( On W())

      proof

        let x be object;

        assume x in ( rng psi);

        then

        consider y be object such that

         A2: y in ( dom psi) and

         A3: x = (psi . y) by FUNCT_1:def 3;

        reconsider y as Ordinal by A2;

        x = F(y) by A1, A2, A3;

        hence thesis by ORDINAL1:def 9;

      end;

      then

      reconsider psi as Ordinal-Sequence of W() by A1, FUNCT_2:def 1, RELSET_1: 4;

      take psi;

      let a be Ordinal of W();

      a in ( On W()) by ORDINAL1:def 9;

      hence thesis by A1;

    end;

    definition

      let W;

      :: ORDINAL4:def2

      func 0-element_of W -> Ordinal of W equals {} ;

      correctness

      proof

        

         A1: ( On W) c= W by ORDINAL2: 7;

         {} in ( On W) by ORDINAL3: 8;

        then

        reconsider A = {} as Ordinal of W by A1;

        A = {} ;

        hence thesis;

      end;

      :: ORDINAL4:def3

      func 1-element_of W -> non empty Ordinal of W equals 1;

      correctness

      proof

        

         A2: ( On W) c= W by ORDINAL2: 7;

         {} in ( On W) by ORDINAL3: 8;

        then

        reconsider A = 1 as Ordinal of W by A2, Lm3, CLASSES2: 5;

        A = 1;

        hence thesis by Lm9;

      end;

      let phi, A1;

      :: original: .

      redefine

      func phi . A1 -> Ordinal of W ;

      coherence

      proof

        reconsider B = (phi . A1) as Ordinal;

        

         A3: ( dom phi) = ( On W) by FUNCT_2:def 1;

        

         A4: ( rng phi) c= ( On W) by RELAT_1:def 19;

        A1 in ( On W) by ORDINAL1:def 9;

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

        then

         A5: B in ( On W) by A4;

        ( On W) c= W by ORDINAL2: 7;

        hence thesis by A5;

      end;

    end

    definition

      let W;

      let p2,p1 be Ordinal-Sequence of W;

      :: original: *

      redefine

      func p1 * p2 -> Ordinal-Sequence of W ;

      coherence

      proof

        

         A1: ( rng p2) c= ( On W) by RELAT_1:def 19;

        

         A2: ( dom p2) = ( On W) by FUNCT_2:def 1;

        ( dom p1) = ( On W) by FUNCT_2:def 1;

        then

         A3: ( dom (p1 * p2)) = ( On W) by A2, A1, RELAT_1: 27;

        then

        reconsider f = (p1 * p2) as Sequence by ORDINAL1:def 7;

        

         A4: ( rng p1) c= ( On W) by RELAT_1:def 19;

        ( rng (p1 * p2)) c= ( rng p1) by RELAT_1: 26;

        then ( rng f) c= ( On W) by A4;

        hence thesis by A3, FUNCT_2:def 1, RELSET_1: 4;

      end;

    end

    theorem :: ORDINAL4:33

    ( 0-element_of W) = {} & ( 1-element_of W) = 1;

    definition

      let W, A1;

      :: original: succ

      redefine

      func succ A1 -> non empty Ordinal of W ;

      coherence by CLASSES2: 5;

      let B1;

      :: original: +^

      redefine

      func A1 +^ B1 -> Ordinal of W ;

      coherence

      proof

        defpred P[ Ordinal] means $1 in W implies (A1 +^ $1) in W;

        

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

        proof

          let B such that

           A2: for C st C in B holds C in W implies (A1 +^ C) in W and

           A3: B in W;

           [:B, {( 1-element_of W)}:] in W by A3, CLASSES2: 61;

          then ( [:A1, {( 0-element_of W)}:] \/ [:B, {( 1-element_of W)}:]) in W by CLASSES2: 60;

          then

           A4: ( card ( [:A1, {( 0-element_of W)}:] \/ [:B, {( 1-element_of W)}:])) in ( card W) by CLASSES2: 1;

          

           A5: (A1 +^ B) c= W

          proof

            let x be object;

            assume

             A6: x in (A1 +^ B);

            then

            reconsider A = x as Ordinal;

             A7:

            now

              

               A8: B c= W by A3, ORDINAL1:def 2;

              assume A1 c= A;

              then

              consider C such that

               A9: A = (A1 +^ C) by ORDINAL3: 27;

              C in B by A6, A9, ORDINAL3: 22;

              hence thesis by A2, A9, A8;

            end;

            

             A10: A in A1 or A1 c= A by ORDINAL1: 16;

            A1 c= W by ORDINAL1:def 2;

            hence thesis by A10, A7;

          end;

          ( card (A1 +^ B)) = ( card ( [:A1, {( 0-element_of W)}:] \/ [:B, {( 1-element_of W)}:])) by CARD_2: 9;

          hence thesis by A4, A5, CLASSES1: 1;

        end;

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

        hence thesis;

      end;

    end

    definition

      let W, A1, B1;

      :: original: *^

      redefine

      func A1 *^ B1 -> Ordinal of W ;

      coherence

      proof

        defpred P[ Ordinal] means $1 in W implies ($1 *^ B1) in W;

        

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

        proof

          let A such that

           A2: for C st C in A holds C in W implies (C *^ B1) in W and

           A3: A in W;

           [:A, B1:] in W by A3, CLASSES2: 61;

          then

           A4: ( card [:A, B1:]) in ( card W) by CLASSES2: 1;

          

           A5: (A *^ B1) c= W

          proof

            let x be object;

            

             A6: B1 c= W by ORDINAL1:def 2;

            assume

             A7: x in (A *^ B1);

            then

            reconsider B = x as Ordinal;

            B1 <> {} by A7, ORDINAL2: 38;

            then

            consider C, D such that

             A8: B = ((C *^ B1) +^ D) and

             A9: D in B1 by ORDINAL3: 47;

            (C *^ B1) c= B by A8, ORDINAL3: 24;

            then (C *^ B1) in (A *^ B1) by A7, ORDINAL1: 12;

            then

             A10: C in A by ORDINAL3: 34;

            A c= W by A3, ORDINAL1:def 2;

            then

            reconsider CB = (C *^ B1), D as Ordinal of W by A2, A9, A6, A10;

            x = (CB +^ D) by A8;

            hence thesis;

          end;

          ( card (A *^ B1)) = ( card [:A, B1:]) by CARD_2: 11;

          hence thesis by A4, A5, CLASSES1: 1;

        end;

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

        hence thesis;

      end;

    end

    theorem :: ORDINAL4:34

    

     Th34: A1 in ( dom phi)

    proof

      ( dom phi) = ( On W) by FUNCT_2:def 1;

      hence thesis by ORDINAL1:def 9;

    end;

    theorem :: ORDINAL4:35

    

     Th35: ( dom fi) in W & ( rng fi) c= W implies ( sup fi) in W

    proof

      assume that

       A1: ( dom fi) in W and

       A2: ( rng fi) c= W;

      ex A st ( rng fi) c= A by ORDINAL2:def 4;

      then for x st x in ( rng fi) holds x is Ordinal;

      then

      reconsider B = ( union ( rng fi)) as epsilon-transitive epsilon-connected set by ORDINAL1: 23;

      

       A3: ( rng fi) = (fi .: ( dom fi)) by RELAT_1: 113;

      

       A4: ( sup fi) c= ( succ B)

      proof

        let x be object;

        assume

         A5: x in ( sup fi);

        then

        reconsider A = x as Ordinal;

        consider C such that

         A6: C in ( rng fi) and

         A7: A c= C by A5, ORDINAL2: 21;

        C c= ( union ( rng fi)) by A6, ZFMISC_1: 74;

        then A c= B by A7;

        hence thesis by ORDINAL1: 22;

      end;

      ( card ( dom fi)) in ( card W) by A1, CLASSES2: 1;

      then ( card ( rng fi)) in ( card W) by A3, CARD_1: 67, ORDINAL1: 12;

      then ( rng fi) in W by A2, CLASSES1: 1;

      then ( union ( rng fi)) in W by CLASSES2: 59;

      then ( succ B) in W by CLASSES2: 5;

      hence thesis by A4, CLASSES1:def 1;

    end;

    reserve L for Sequence;

    theorem :: ORDINAL4:36

    phi is increasing & phi is continuous & omega in W implies ex A st A in ( dom phi) & (phi . A) = A

    proof

      deffunc D( set, set) = {} ;

      assume that

       A1: phi is increasing and

       A2: phi is continuous and

       A3: omega in W;

      deffunc C( set, set) = (phi . $2);

      reconsider N = (phi . ( 0-element_of W)) as Ordinal;

      consider L such that

       A4: ( dom L) = omega and

       A5: 0 in omega implies (L . 0 ) = N and

       A6: for A st ( succ A) in omega holds (L . ( succ A)) = C(A,.) and for A st A in omega & A <> 0 & A is limit_ordinal holds (L . A) = D(A,|) from ORDINAL2:sch 5;

      defpred P[ Ordinal] means $1 in ( dom L) implies (L . $1) is Ordinal of W;

      

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

      proof

        let A such that

         A8: A in ( dom L) implies (L . A) is Ordinal of W and

         A9: ( succ A) in ( dom L);

        A in ( succ A) by ORDINAL1: 6;

        then

        reconsider x = (L . A) as Ordinal of W by A8, A9, ORDINAL1: 10;

        (L . ( succ A)) = (phi . x) by A4, A6, A9;

        hence thesis;

      end;

      

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

      proof

        let A such that

         A11: A <> 0 and

         A12: A is limit_ordinal and for B st B in A holds B in ( dom L) implies (L . B) is Ordinal of W and

         A13: A in ( dom L);

         {} in A by A11, ORDINAL3: 8;

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

        hence thesis by A4, A13, ORDINAL1: 5;

      end;

      

       A14: P[ 0 ] by A4, A5;

      

       A15: for A holds P[A] from ORDINAL2:sch 1( A14, A7, A10);

      ( rng L) c= ( sup ( rng L))

      proof

        let x be object;

        assume

         A16: x in ( rng L);

        then

        consider y be object such that

         A17: y in ( dom L) and

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

        reconsider y as Ordinal by A17;

        reconsider A = (L . y) as Ordinal of W by A15, A17;

        A in ( sup ( rng L)) by A16, A18, ORDINAL2: 19;

        hence thesis by A18;

      end;

      then

      reconsider L as Ordinal-Sequence by ORDINAL2:def 4;

      

       A19: ( dom phi) = ( On W) by FUNCT_2:def 1;

      assume

       A20: not thesis;

       A21:

      now

        let A1;

        A1 in ( dom phi) by Th34;

        then

         A22: A1 c= (phi . A1) by A1, Th10;

        A1 <> (phi . A1) by A20, Th34;

        then A1 c< (phi . A1) by A22;

        hence A1 in (phi . A1) by ORDINAL1: 11;

      end;

      L is increasing

      proof

        let A, B;

        assume that

         A23: A in B and

         A24: B in ( dom L);

        defpred P[ Ordinal] means (A +^ $1) in omega & $1 <> {} implies (L . A) in (L . (A +^ $1));

        

         A25: for B st B <> 0 & B is limit_ordinal & for C st C in B holds P[C] holds P[B]

        proof

          let B such that

           A26: B <> 0 and

           A27: B is limit_ordinal and for C st C in B holds (A +^ C) in omega & C <> {} implies (L . A) in (L . (A +^ C)) and

           A28: (A +^ B) in omega and

           A29: B <> {} ;

          (A +^ B) <> {} by A29, ORDINAL3: 26;

          then

           A30: {} in (A +^ B) by ORDINAL3: 8;

          (A +^ B) is limit_ordinal by A26, A27, ORDINAL3: 29;

          then omega c= (A +^ B) by A30, ORDINAL1:def 11;

          hence thesis by A28, ORDINAL1: 5;

        end;

        

         A31: for C st P[C] holds P[( succ C)]

        proof

          let C such that

           A32: (A +^ C) in omega & C <> {} implies (L . A) in (L . (A +^ C)) and

           A33: (A +^ ( succ C)) in omega and ( succ C) <> {} ;

          

           A34: (A +^ ( succ C)) = ( succ (A +^ C)) by ORDINAL2: 28;

          

           A35: (A +^ C) in ( succ (A +^ C)) by ORDINAL1: 6;

          then

          reconsider D = (L . (A +^ C)) as Ordinal of W by A4, A15, A33, A34, ORDINAL1: 10;

          

           A36: D in (phi . D) by A21;

          (L . (A +^ ( succ C))) = (phi . D) by A6, A33, A34;

          hence thesis by A32, A33, A35, A34, A36, ORDINAL1: 10, ORDINAL2: 27;

        end;

        

         A37: P[ 0 ];

        

         A38: for C holds P[C] from ORDINAL2:sch 1( A37, A31, A25);

        ex C st B = (A +^ C) & C <> {} by A23, ORDINAL3: 28;

        hence thesis by A4, A24, A38;

      end;

      then

       A39: ( sup L) is limit_ordinal by A4, Lm2, Th16;

      

       A40: ( rng L) c= W

      proof

        let x be object;

        assume x in ( rng L);

        then

        consider y be object such that

         A41: y in ( dom L) and

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

        reconsider y as Ordinal by A41;

        (L . y) is Ordinal of W by A15, A41;

        hence thesis by A42;

      end;

      then

      reconsider S = ( sup L) as Ordinal of W by A3, A4, Th35;

      set fi = (phi | ( sup L));

      N in ( rng L) by A4, A5, Lm1, FUNCT_1:def 3;

      then

       A43: ( sup L) <> {} by ORDINAL2: 19;

      

       A44: S in ( On W) by ORDINAL1:def 9;

      then

       A45: (phi . S) is_limes_of fi by A2, A43, A39, A19;

      S c= ( dom phi) by A44, A19, ORDINAL1:def 2;

      then

       A46: ( dom fi) = S by RELAT_1: 62;

      

       A47: ( sup fi) c= ( sup L)

      proof

        let x be object;

        assume

         A48: x in ( sup fi);

        then

        reconsider A = x as Ordinal;

        consider B such that

         A49: B in ( rng fi) and

         A50: A c= B by A48, ORDINAL2: 21;

        consider y be object such that

         A51: y in ( dom fi) and

         A52: B = (fi . y) by A49, FUNCT_1:def 3;

        reconsider y as Ordinal by A51;

        consider C such that

         A53: C in ( rng L) and

         A54: y c= C by A46, A51, ORDINAL2: 21;

        reconsider C1 = C as Ordinal of W by A40, A53;

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

        then y in C1 & C1 in ( dom phi) or y = C by A19, A54, ORDINAL1: 11, ORDINAL1:def 9;

        then

         A55: (phi . y) in (phi . C1) or y = C1 by A1;

        B = (phi . y) by A51, A52, FUNCT_1: 47;

        then

         A56: B c= (phi . C1) by A55, ORDINAL1:def 2;

        consider z be object such that

         A57: z in ( dom L) and

         A58: C = (L . z) by A53, FUNCT_1:def 3;

        reconsider z as Ordinal by A57;

        

         A59: ( succ z) in omega by A4, A57, Lm2, ORDINAL1: 28;

        then

         A60: (L . ( succ z)) in ( rng L) by A4, FUNCT_1:def 3;

        (L . ( succ z)) = (phi . C) by A6, A58, A59;

        then (phi . C1) in ( sup L) by A60, ORDINAL2: 19;

        then B in ( sup L) by A56, ORDINAL1: 12;

        hence thesis by A50, ORDINAL1: 12;

      end;

      fi is increasing

      proof

        

         A61: ( dom fi) c= ( dom phi) by RELAT_1: 60;

        let A, B;

        assume that

         A62: A in B and

         A63: B in ( dom fi);

        

         A64: (fi . B) = (phi . B) by A63, FUNCT_1: 47;

        (fi . A) = (phi . A) by A62, A63, FUNCT_1: 47, ORDINAL1: 10;

        hence thesis by A1, A62, A63, A61, A64;

      end;

      

      then ( sup fi) = ( lim fi) by A43, A39, A46, Th8

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

      then not S in (phi . S) by A47, ORDINAL1: 5;

      hence contradiction by A21;

    end;

    begin

    reserve e,u for set;

    theorem :: ORDINAL4:37

    A is_cofinal_with B & B is_cofinal_with C implies A is_cofinal_with C

    proof

      given xi1 be Ordinal-Sequence such that

       A1: ( dom xi1) = B and

       A2: ( rng xi1) c= A and

       A3: xi1 is increasing and

       A4: A = ( sup xi1);

      given xi2 be Ordinal-Sequence such that

       A5: ( dom xi2) = C and

       A6: ( rng xi2) c= B and

       A7: xi2 is increasing and

       A8: B = ( sup xi2);

      consider xi be Ordinal-Sequence such that

       A9: xi = (xi1 * xi2) and

       A10: xi is increasing by A3, A7, Th13;

      take xi;

      thus

       A11: ( dom xi) = C by A1, A5, A6, A9, RELAT_1: 27;

      ( rng xi) c= ( rng xi1) by A9, RELAT_1: 26;

      hence

       A12: ( rng xi) c= A & xi is increasing by A2, A10;

      thus A c= ( sup xi)

      proof

        let a be object;

        assume

         A13: a in A;

        then

        reconsider a as Ordinal;

        consider b be Ordinal such that

         A14: b in ( rng xi1) and

         A15: a c= b by A4, A13, ORDINAL2: 21;

        consider e be object such that

         A16: e in B and

         A17: b = (xi1 . e) by A1, A14, FUNCT_1:def 3;

        reconsider e as Ordinal by A16;

        consider c be Ordinal such that

         A18: c in ( rng xi2) and

         A19: e c= c by A8, A16, ORDINAL2: 21;

        consider u be object such that

         A20: u in C and

         A21: c = (xi2 . u) by A5, A18, FUNCT_1:def 3;

        reconsider u as Ordinal by A20;

        

         A22: (xi1 . c) = (xi . u) by A9, A11, A20, A21, FUNCT_1: 12;

        (xi . u) in ( rng xi) by A11, A20, FUNCT_1:def 3;

        then

         A23: (xi . u) in ( sup xi) by ORDINAL2: 19;

        (xi1 . e) c= (xi1 . c) by A1, A3, A6, A18, A19, Th9;

        hence thesis by A15, A17, A22, A23, ORDINAL1: 12, XBOOLE_1: 1;

      end;

      ( sup ( rng xi)) c= ( sup A) by A12, ORDINAL2: 22;

      hence thesis by ORDINAL2: 18;

    end;

    theorem :: ORDINAL4:38

    A is_cofinal_with B implies (A is limit_ordinal iff B is limit_ordinal)

    proof

      given psi such that

       A1: ( dom psi) = B and

       A2: ( rng psi) c= A and

       A3: psi is increasing and

       A4: A = ( sup psi);

      thus A is limit_ordinal implies B is limit_ordinal

      proof

        assume

         A5: A is limit_ordinal;

        now

          let C;

          reconsider c = (psi . C) as Ordinal;

          assume

           A6: C in B;

          then (psi . C) in ( rng psi) by A1, FUNCT_1:def 3;

          then ( succ c) in A by A2, A5, ORDINAL1: 28;

          then

          consider b be Ordinal such that

           A7: b in ( rng psi) and

           A8: ( succ c) c= b by A4, ORDINAL2: 21;

          consider e be object such that

           A9: e in B and

           A10: b = (psi . e) by A1, A7, FUNCT_1:def 3;

          reconsider e as Ordinal by A9;

          c in ( succ c) by ORDINAL1: 6;

          then not e c= C by A1, A3, A6, A8, A10, Th9, ORDINAL1: 5;

          then C in e by ORDINAL1: 16;

          then ( succ C) c= e by ORDINAL1: 21;

          hence ( succ C) in B by A9, ORDINAL1: 12;

        end;

        hence thesis by ORDINAL1: 28;

      end;

      thus thesis by A1, A3, A4, Th16;

    end;

    registration

      let D;

      let f,g be Sequence of D;

      cluster (f ^ g) -> D -valued;

      coherence

      proof

        ( rng f) c= D & ( rng g) c= D by RELAT_1:def 19;

        then

         A1: (( rng f) \/ ( rng g)) c= D by XBOOLE_1: 8;

        ( rng (f ^ g)) c= (( rng f) \/ ( rng g)) by Th2;

        hence ( rng (f ^ g)) c= D by A1;

      end;

    end

    theorem :: ORDINAL4:39

    for A,B be Sequence holds ( rng A) c= ( rng (A ^ B)) by Th7A;

    theorem :: ORDINAL4:40

    for A,B be Sequence holds ( rng B) c= ( rng (A ^ B)) by Th8A;