arrow.miz



    begin

    definition

      let A,B9 be non empty set;

      let B be non empty Subset of B9;

      let f be Function of A, B;

      let x be Element of A;

      :: original: .

      redefine

      func f . x -> Element of B ;

      coherence

      proof

        thus (f . x) is Element of B;

      end;

    end

    theorem :: ARROW:1

    

     Th1: for A be finite set st ( card A) >= 2 holds for a be Element of A holds ex b be Element of A st b <> a

    proof

      let A9 be finite set;

      assume

       A1: ( card A9) >= 2;

      then

      reconsider A = A9 as finite non empty set by CARD_1: 27;

      let a be Element of A9;

       {a} c= A by ZFMISC_1: 31;

      

      then ( card (A \ {a})) = (( card A) - ( card {a})) by CARD_2: 44

      .= (( card A) - 1) by CARD_1: 30;

      then ( card (A \ {a})) <> 0 by A1;

      then

      consider b be object such that

       A2: b in (A \ {a}) by CARD_1: 27, XBOOLE_0:def 1;

      reconsider b as Element of A9 by A2;

      take b;

       not b in {a} by A2, XBOOLE_0:def 5;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: ARROW:2

    

     Th2: for A be finite set st ( card A) >= 3 holds for a,b be Element of A holds ex c be Element of A st c <> a & c <> b

    proof

      let A9 be finite set;

      assume

       A1: ( card A9) >= 3;

      then

      reconsider A = A9 as finite non empty set by CARD_1: 27;

      let a,b be Element of A9;

       {a, b} c= A by ZFMISC_1: 32;

      then

       A2: ( card (A \ {a, b})) = (( card A) - ( card {a, b})) by CARD_2: 44;

      ( card {a, b}) <= 2 by CARD_2: 50;

      then ( card (A \ {a, b})) >= (3 - 2) by A1, A2, XREAL_1: 13;

      then ( card (A \ {a, b})) <> 0 ;

      then

      consider c be object such that

       A3: c in (A \ {a, b}) by CARD_1: 27, XBOOLE_0:def 1;

      reconsider c as Element of A9 by A3;

      take c;

       not c in {a, b} by A3, XBOOLE_0:def 5;

      hence thesis by TARSKI:def 2;

    end;

    begin

    reserve A for non empty set;

    reserve a,b,c,x,y,z for Element of A;

    definition

      let A;

      defpred P[ set] means $1 is Relation of A & (for a, b holds [a, b] in $1 or [b, a] in $1) & (for a, b, c st [a, b] in $1 & [b, c] in $1 holds [a, c] in $1);

      defpred Q[ set] means for R be set holds R in $1 iff P[R];

      :: ARROW:def1

      func LinPreorders A -> set means

      : Def1: for R be set holds R in it iff R is Relation of A & (for a, b holds [a, b] in R or [b, a] in R) & for a, b, c st [a, b] in R & [b, c] in R holds [a, c] in R;

      existence

      proof

        consider it0 be set such that

         A1: for R be set holds R in it0 iff R in ( bool [:A, A:]) & P[R] from XFAMILY:sch 1;

        take it0;

        let R be set;

        thus R in it0 implies P[R] by A1;

        assume

         A2: P[R];

         [:A, A:] in ( bool [:A, A:]) by ZFMISC_1:def 1;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let it1,it2 be set;

        assume that

         A3: Q[it1] and

         A4: Q[it2];

        now

          let R be object;

          reconsider RR = R as set by TARSKI: 1;

          R in it1 iff P[RR] by A3;

          hence R in it1 iff R in it2 by A4;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    registration

      let A;

      cluster ( LinPreorders A) -> non empty;

      coherence

      proof

         [:A, A:] c= [:A, A:];

        then

        reconsider R = [:A, A:] as Relation of A;

        (for a, b holds [a, b] in R or [b, a] in R) & for a, b, c st [a, b] in R & [b, c] in R holds [a, c] in R by ZFMISC_1: 87;

        hence thesis by Def1;

      end;

    end

    definition

      let A;

      defpred P[ set] means for a, b st [a, b] in $1 & [b, a] in $1 holds a = b;

      defpred Q[ set] means for R be Element of ( LinPreorders A) holds R in $1 iff P[R];

      :: ARROW:def2

      func LinOrders A -> Subset of ( LinPreorders A) means

      : Def2: for R be Element of ( LinPreorders A) holds R in it iff for a, b st [a, b] in R & [b, a] in R holds a = b;

      existence

      proof

        consider it0 be set such that

         A1: for R be set holds R in it0 iff R in ( LinPreorders A) & P[R] from XFAMILY:sch 1;

        for R be object st R in it0 holds R in ( LinPreorders A) by A1;

        then

        reconsider it0 as Subset of ( LinPreorders A) by TARSKI:def 3;

        take it0;

        let R be Element of ( LinPreorders A);

        thus R in it0 implies P[R] by A1;

        assume P[R];

        hence thesis by A1;

      end;

      uniqueness

      proof

        let it1,it2 be Subset of ( LinPreorders A);

        assume that

         A2: Q[it1] and

         A3: Q[it2];

        now

          let R be Element of ( LinPreorders A);

          R in it1 iff P[R] by A2;

          hence R in it1 iff R in it2 by A3;

        end;

        hence thesis by SUBSET_1: 3;

      end;

    end

    registration

      let A be set;

      cluster connected for Order of A;

      existence

      proof

        consider R9 be Relation such that

         A1: R9 well_orders A by WELLORD2: 17;

        set R = (R9 |_2 A);

        

         A2: R is well-ordering by A1, WELLORD2: 16;

        reconsider R as Relation of A by XBOOLE_1: 17;

        now

          let a be object;

          assume

           A3: a in A;

          R9 is_reflexive_in A by A1;

          then

           A4: [a, a] in R9 by A3, RELAT_2:def 1;

           [a, a] in [:A, A:] by A3, ZFMISC_1:def 2;

          then [a, a] in R by A4, XBOOLE_0:def 4;

          hence a in ( dom R) by XTUPLE_0:def 12;

        end;

        then A c= ( dom R) by TARSKI:def 3;

        then ( dom R) = A by XBOOLE_0:def 10;

        then

        reconsider R as Order of A by A2, PARTFUN1:def 2;

        take R;

        thus thesis by A2;

      end;

    end

    definition

      let A;

      :: original: LinOrders

      redefine

      :: ARROW:def3

      func LinOrders A means

      : Def3: for R be set holds R in it iff R is connected Order of A;

      compatibility

      proof

         A1:

        now

          let R be set;

          assume

           A2: R in ( LinOrders A);

          then

          reconsider R9 = R as Relation of A by Def1;

          now

            let a be object;

            assume a in A;

            then [a, a] in R by A2, Def1;

            hence a in ( dom R9) by XTUPLE_0:def 12;

          end;

          then A c= ( dom R9) by TARSKI:def 3;

          then

           A3: ( dom R9) = A by XBOOLE_0:def 10;

          now

            let a be object;

            assume a in A;

            then [a, a] in R by A2, Def1;

            hence a in ( rng R9) by XTUPLE_0:def 13;

          end;

          then A c= ( rng R9) by TARSKI:def 3;

          then

           A4: ( field R9) = (A \/ A) by A3, XBOOLE_0:def 10;

          for a,b be object st a in A & b in A & a <> b holds [a, b] in R or [b, a] in R by A2, Def1;

          then

           A5: R9 is_connected_in A by RELAT_2:def 6;

          for a be object st a in A holds [a, a] in R by A2, Def1;

          then

           A6: R9 is_reflexive_in A by RELAT_2:def 1;

          for a,b be object st a in A & b in A & [a, b] in R & [b, a] in R holds a = b by A2, Def2;

          then

           A7: R9 is_antisymmetric_in A by RELAT_2:def 4;

          for a,b,c be object st a in A & b in A & c in A & [a, b] in R & [b, c] in R holds [a, c] in R by A2, Def1;

          then R9 is_transitive_in A by RELAT_2:def 8;

          hence R is connected Order of A by A3, A4, A5, A6, A7, PARTFUN1:def 2, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 14, RELAT_2:def 16;

        end;

         A8:

        now

          let R be set;

          assume

           A9: R is connected Order of A;

          then

          reconsider R9 = R as connected Order of A;

           A10:

          now

            let a, b;

            ( dom R9) = A by PARTFUN1:def 2;

            then A c= (( dom R9) \/ ( rng R9)) by XBOOLE_1: 7;

            then

             A11: ( field R9) = A by XBOOLE_0:def 10;

            

             A12: R9 is_connected_in ( field R9) & R9 is_reflexive_in ( field R9) by RELAT_2:def 9, RELAT_2:def 14;

            a = b or a <> b;

            hence [a, b] in R or [b, a] in R by A11, A12, RELAT_2:def 1, RELAT_2:def 6;

          end;

          for a, b, c st [a, b] in R & [b, c] in R holds [a, c] in R by A9, ORDERS_1: 5;

          then

           A13: R in ( LinPreorders A) by A9, A10, Def1;

          for a, b st [a, b] in R & [b, a] in R holds a = b by A9, ORDERS_1: 4;

          hence R in ( LinOrders A) by A13, Def2;

        end;

        let it0 be Subset of ( LinPreorders A);

        thus it0 = ( LinOrders A) implies for R be set holds R in it0 iff R is connected Order of A by A1, A8;

        assume

         A14: for R be set holds R in it0 iff R is connected Order of A;

        now

          let R be object;

          R in it0 iff R is connected Order of A by A14;

          hence R in it0 iff R in ( LinOrders A) by A1, A8;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    registration

      let A;

      cluster ( LinOrders A) -> non empty;

      coherence

      proof

        set R = the connected Order of A;

        R in ( LinOrders A) by Def3;

        hence thesis;

      end;

    end

    registration

      let A;

      cluster -> Relation-like for Element of ( LinPreorders A);

      coherence by Def1;

      cluster -> Relation-like for Element of ( LinOrders A);

      coherence ;

    end

    reserve o,o9 for Element of ( LinPreorders A);

    reserve o99 for Element of ( LinOrders A);

    definition

      let o be Relation, a,b be set;

      :: ARROW:def4

      pred a <=_ o,b means [a, b] in o;

    end

    notation

      let o be Relation, a,b be set;

      synonym b >=_ o,a for a <=_ o,b;

      antonym b <_ o,a for a <=_ o,b;

      antonym a >_ o,b for a <=_ o,b;

    end

    theorem :: ARROW:3

    

     Th3: a <=_ (o,a) by Def1;

    theorem :: ARROW:4

    

     Th4: a <=_ (o,b) or b <=_ (o,a) by Def1;

    theorem :: ARROW:5

    

     Th5: (a <=_ (o,b) or a <_ (o,b)) & (b <=_ (o,c) or b <_ (o,c)) implies a <=_ (o,c)

    proof

      assume a <=_ (o,b) or a <_ (o,b);

      then a <=_ (o,b) by Th4;

      then

       A1: [a, b] in o;

      assume b <=_ (o,c) or b <_ (o,c);

      then b <=_ (o,c) by Th4;

      then [b, c] in o;

      hence [a, c] in o by A1, Def1;

    end;

    theorem :: ARROW:6

    

     Th6: a <=_ (o99,b) & b <=_ (o99,a) implies a = b by Def2;

    theorem :: ARROW:7

    

     Th7: a <> b & b <> c & a <> c implies ex o st a <_ (o,b) & b <_ (o,c)

    proof

      assume that

       A1: a <> b & b <> c and

       A2: a <> c;

      defpred P[ set, set] means ($1 = a or $2 <> a) & ($1 <> c or $2 = c);

      consider R be Relation of A such that

       A3: for x, y holds [x, y] in R iff P[x, y] from RELSET_1:sch 2;

       A4:

      now

        let x, y;

         P[x, y] or P[y, x] by A2;

        hence [x, y] in R or [y, x] in R by A3;

      end;

      now

        let x, y, z;

        assume [x, y] in R & [y, z] in R;

        then P[x, y] & P[y, z] by A3;

        hence [x, z] in R by A3;

      end;

      then

      reconsider o = R as Element of ( LinPreorders A) by A4, Def1;

      take o;

      ( not [b, a] in R) & not [c, b] in R by A1, A3;

      hence thesis;

    end;

    theorem :: ARROW:8

    

     Th8: ex o st for a st a <> b holds b <_ (o,a)

    proof

      defpred P[ set, set] means $1 = b or $2 <> b;

      consider R be Relation of A such that

       A1: for x, y holds [x, y] in R iff P[x, y] from RELSET_1:sch 2;

       A2:

      now

        let x, y;

         P[x, y] or P[y, x];

        hence [x, y] in R or [y, x] in R by A1;

      end;

      now

        let x, y, z;

        assume that

         A3: [x, y] in R and

         A4: [y, z] in R;

         P[y, z] by A1, A4;

        hence [x, z] in R by A1, A3;

      end;

      then

      reconsider o = R as Element of ( LinPreorders A) by A2, Def1;

      take o;

      let a;

      assume a <> b;

      then not [a, b] in R by A1;

      hence thesis;

    end;

    theorem :: ARROW:9

    

     Th9: ex o st for a st a <> b holds a <_ (o,b)

    proof

      defpred P[ set, set] means $1 <> b or $2 = b;

      consider R be Relation of A such that

       A1: for x, y holds [x, y] in R iff P[x, y] from RELSET_1:sch 2;

       A2:

      now

        let x, y;

         P[x, y] or P[y, x];

        hence [x, y] in R or [y, x] in R by A1;

      end;

      now

        let x, y, z;

        assume that

         A3: [x, y] in R and

         A4: [y, z] in R;

         P[x, y] by A1, A3;

        hence [x, z] in R by A1, A4;

      end;

      then

      reconsider o = R as Element of ( LinPreorders A) by A2, Def1;

      take o;

      let a;

      assume a <> b;

      then not [b, a] in R by A1;

      hence thesis;

    end;

    theorem :: ARROW:10

    

     Th10: a <> b & a <> c implies ex o st a <_ (o,b) & a <_ (o,c) & (b <_ (o,c) iff b <_ (o9,c)) & (c <_ (o,b) iff c <_ (o9,b))

    proof

      assume

       A1: a <> b & a <> c;

      defpred P[ Element of A, Element of A] means $1 = a or ($1 <=_ (o9,$2) & $2 <> a);

      consider R be Relation of A such that

       A2: for x, y holds [x, y] in R iff P[x, y] from RELSET_1:sch 2;

       A3:

      now

        let x, y;

         P[x, y] or P[y, x] by Th4;

        hence [x, y] in R or [y, x] in R by A2;

      end;

      now

        let x, y, z;

        assume [x, y] in R & [y, z] in R;

        then P[x, y] & P[y, z] by A2;

        then P[x, z] by Th5;

        hence [x, z] in R by A2;

      end;

      then

      reconsider o = R as Element of ( LinPreorders A) by A3, Def1;

      take o;

      

       A4: ( not [b, a] in R) & not [c, a] in R by A1, A2;

      

       A5: not [c, b] in R iff b <_ (o9,c) by A1, A2;

       not [b, c] in R iff c <_ (o9,b) by A1, A2;

      hence thesis by A4, A5;

    end;

    theorem :: ARROW:11

    

     Th11: a <> b & a <> c implies ex o st b <_ (o,a) & c <_ (o,a) & (b <_ (o,c) iff b <_ (o9,c)) & (c <_ (o,b) iff c <_ (o9,b))

    proof

      assume

       A1: a <> b & a <> c;

      defpred P[ Element of A, Element of A] means ($1 <> a & $1 <=_ (o9,$2)) or $2 = a;

      consider R be Relation of A such that

       A2: for x, y holds [x, y] in R iff P[x, y] from RELSET_1:sch 2;

       A3:

      now

        let x, y;

         P[x, y] or P[y, x] by Th4;

        hence [x, y] in R or [y, x] in R by A2;

      end;

      now

        let x, y, z;

        assume [x, y] in R & [y, z] in R;

        then P[x, y] & P[y, z] by A2;

        then P[x, z] by Th5;

        hence [x, z] in R by A2;

      end;

      then

      reconsider o = R as Element of ( LinPreorders A) by A3, Def1;

      take o;

      

       A4: ( not [a, b] in R) & not [a, c] in R by A1, A2;

      

       A5: not [c, b] in R iff b <_ (o9,c) by A1, A2;

       not [b, c] in R iff c <_ (o9,b) by A1, A2;

      hence thesis by A4, A5;

    end;

    theorem :: ARROW:12

    for o,o9 be Element of ( LinOrders A) holds (a <_ (o,b) iff a <_ (o9,b)) & (b <_ (o,a) iff b <_ (o9,a)) iff (a <_ (o,b) iff a <_ (o9,b))

    proof

      let o,o9 be Element of ( LinOrders A);

      thus (a <_ (o,b) iff a <_ (o9,b)) & (b <_ (o,a) iff b <_ (o9,a)) implies (a <_ (o,b) iff a <_ (o9,b));

      assume

       A1: a <_ (o,b) iff a <_ (o9,b);

      hence a <_ (o,b) iff a <_ (o9,b);

      hereby

        assume

         A2: b <_ (o,a);

        then a <> b by Th4;

        hence b <_ (o9,a) by A1, A2, Th4, Th6;

      end;

      assume

       A3: b <_ (o9,a);

      then a <> b by Th4;

      hence thesis by A1, A3, Th4, Th6;

    end;

    theorem :: ARROW:13

    

     Th13: for o be Element of ( LinOrders A), o9 be Element of ( LinPreorders A) holds (for a, b st a <_ (o,b) holds a <_ (o9,b)) iff for a, b holds a <_ (o,b) iff a <_ (o9,b)

    proof

      let o be Element of ( LinOrders A), o9 be Element of ( LinPreorders A);

      hereby

        assume

         A1: for a, b st a <_ (o,b) holds a <_ (o9,b);

        let a, b;

        per cases by Th6;

          suppose a <_ (o,b);

          hence a <_ (o,b) iff a <_ (o9,b) by A1;

        end;

          suppose a = b;

          hence a <_ (o,b) iff a <_ (o9,b) by Th3;

        end;

          suppose

           A2: b <_ (o,a);

          then b <_ (o9,a) by A1;

          hence a <_ (o,b) iff a <_ (o9,b) by A2, Th4;

        end;

      end;

      thus thesis;

    end;

    begin

    reserve A,N for finite non empty set;

    reserve a,b,c,d,a9,c9 for Element of A;

    reserve i,n,nb,nc for Element of N;

    reserve o,oI,oII for Element of ( LinPreorders A);

    reserve p,p9,pI,pII,pI9,pII9 for Element of ( Funcs (N,( LinPreorders A)));

    reserve f for Function of ( Funcs (N,( LinPreorders A))), ( LinPreorders A);

    reserve k,k0 for Nat;

    theorem :: ARROW:14

    

     Th14: (for p, a, b st for i holds a <_ ((p . i),b) holds a <_ ((f . p),b)) & (for p, p9, a, b st for i holds (a <_ ((p . i),b) iff a <_ ((p9 . i),b)) & (b <_ ((p . i),a) iff b <_ ((p9 . i),a)) holds a <_ ((f . p),b) iff a <_ ((f . p9),b)) & ( card A) >= 3 implies ex n st for p, a, b st a <_ ((p . n),b) holds a <_ ((f . p),b)

    proof

      assume that

       A1: for p, a, b st for i holds a <_ ((p . i),b) holds a <_ ((f . p),b) and

       A2: for p, p9, a, b st for i holds (a <_ ((p . i),b) iff a <_ ((p9 . i),b)) & (b <_ ((p . i),a) iff b <_ ((p9 . i),a)) holds a <_ ((f . p),b) iff a <_ ((f . p9),b) and

       A3: ( card A) >= 3;

      defpred extreme[ Element of ( LinPreorders A), Element of A] means (for a st a <> $2 holds $2 <_ ($1,a)) or (for a st a <> $2 holds a <_ ($1,$2));

      

       A4: for p, b st for i holds extreme[(p . i), b] holds extreme[(f . p), b]

      proof

        assume not thesis;

        then

        consider p, b such that

         A5: ex a st a <> b & a <=_ ((f . p),b) and

         A6: ex c st c <> b & b <=_ ((f . p),c) and

         A7: for i holds extreme[(p . i), b];

        consider a9 such that

         A8: a9 <> b & a9 <=_ ((f . p),b) by A5;

        consider c9 such that

         A9: b <> c9 & b <=_ ((f . p),c9) by A6;

        ex a, c st a <> b & b <> c & a <> c & a <=_ ((f . p),b) & b <=_ ((f . p),c)

        proof

          per cases ;

            suppose

             A10: a9 <> c9;

            take a9, c9;

            thus thesis by A8, A9, A10;

          end;

            suppose

             A11: a9 = c9;

            consider d such that

             A12: d <> b & d <> a9 by A3, Th2;

            per cases by Th4;

              suppose

               A13: d <=_ ((f . p),b);

              take d, c9;

              thus thesis by A9, A11, A12, A13;

            end;

              suppose

               A14: b <=_ ((f . p),d);

              take a9, d;

              thus thesis by A8, A12, A14;

            end;

          end;

        end;

        then

        consider a, c such that

         A15: a <> b & b <> c and

         A16: a <> c and

         A17: a <=_ ((f . p),b) & b <=_ ((f . p),c);

        defpred P[ Element of N, Element of ( LinPreorders A)] means (a <_ ((p . $1),b) iff a <_ ($2,b)) & (b <_ ((p . $1),a) iff b <_ ($2,a)) & (b <_ ((p . $1),c) iff b <_ ($2,c)) & (c <_ ((p . $1),b) iff c <_ ($2,b)) & c <_ ($2,a);

        

         A18: for i holds ex o st P[i, o]

        proof

          let i;

          per cases by A7;

            suppose for c st c <> b holds b <_ ((p . i),c);

            then

             A19: b <_ ((p . i),a) & b <_ ((p . i),c) by A15;

            consider o such that

             A20: b <_ (o,c) & c <_ (o,a) by A15, A16, Th7;

            take o;

            thus thesis by A19, A20, Th4, Th5;

          end;

            suppose for a st a <> b holds a <_ ((p . i),b);

            then

             A21: a <_ ((p . i),b) & c <_ ((p . i),b) by A15;

            consider o such that

             A22: c <_ (o,a) & a <_ (o,b) by A15, A16, Th7;

            take o;

            thus thesis by A21, A22, Th4, Th5;

          end;

        end;

        consider p9 be Function of N, ( LinPreorders A) such that

         A23: for i holds P[i, (p9 . i)] from FUNCT_2:sch 3( A18);

        reconsider p9 as Element of ( Funcs (N,( LinPreorders A))) by FUNCT_2: 8;

        a <=_ ((f . p9),b) & b <=_ ((f . p9),c) by A2, A17, A23;

        then a <=_ ((f . p9),c) by Th5;

        hence contradiction by A1, A23;

      end;

      

       A24: for b holds ex nb, pI, pII st (for i st i <> nb holds (pI . i) = (pII . i)) & (for i holds extreme[(pI . i), b]) & (for i holds extreme[(pII . i), b]) & (for a st a <> b holds b <_ ((pI . nb),a)) & (for a st a <> b holds a <_ ((pII . nb),b)) & (for a st a <> b holds b <_ ((f . pI),a)) & for a st a <> b holds a <_ ((f . pII),b)

      proof

        consider t be FinSequence such that

         A25: ( rng t) = N and

         A26: t is one-to-one by FINSEQ_4: 58;

        reconsider t as FinSequence of N by A25, FINSEQ_1:def 4;

        let b;

        consider oI such that

         A27: for a st a <> b holds b <_ (oI,a) by Th8;

        consider oII such that

         A28: for a st a <> b holds a <_ (oII,b) by Th9;

        

         A29: for k0 holds ex p st (for k st k in ( dom t) & k < k0 holds (p . (t . k)) = oII) & for k st k in ( dom t) & k >= k0 holds (p . (t . k)) = oI

        proof

          let k0;

          defpred P[ Element of N, Element of ( LinPreorders A)] means ex k st k in ( dom t) & $1 = (t . k) & (k < k0 implies $2 = oII) & (k >= k0 implies $2 = oI);

          

           A30: for i holds ex o st P[i, o]

          proof

            let i;

            consider k be object such that

             A31: k in ( dom t) and

             A32: i = (t . k) by A25, FUNCT_1:def 3;

            reconsider k as Nat by A31;

            per cases ;

              suppose

               A33: k < k0;

              take oII;

              thus thesis by A31, A32, A33;

            end;

              suppose

               A34: k >= k0;

              take oI;

              thus thesis by A31, A32, A34;

            end;

          end;

          consider p be Function of N, ( LinPreorders A) such that

           A35: for i holds P[i, (p . i)] from FUNCT_2:sch 3( A30);

          reconsider p as Element of ( Funcs (N,( LinPreorders A))) by FUNCT_2: 8;

          take p;

          thus for k st k in ( dom t) & k < k0 holds (p . (t . k)) = oII

          proof

            let k;

            assume that

             A36: k in ( dom t) and

             A37: k < k0;

            reconsider i = (t . k) as Element of N by A36, PARTFUN1: 4;

             P[i, (p . i)] by A35;

            hence thesis by A26, A36, A37, FUNCT_1:def 4;

          end;

          let k;

          assume that

           A38: k in ( dom t) and

           A39: k >= k0;

          reconsider i = (t . k) as Element of N by A38, PARTFUN1: 4;

           P[i, (p . i)] by A35;

          hence thesis by A26, A38, A39, FUNCT_1:def 4;

        end;

        defpred Q[ Nat] means for p st (for k st k in ( dom t) & k < $1 holds (p . (t . k)) = oII) & (for k st k in ( dom t) & k >= $1 holds (p . (t . k)) = oI) holds for a st a <> b holds a <_ ((f . p),b);

        reconsider kII9 = (( len t) + 1) as Element of NAT by ORDINAL1:def 12;

        

         A40: Q[kII9]

        proof

          let p;

          assume that

           A41: for k st k in ( dom t) & k < kII9 holds (p . (t . k)) = oII and for k st k in ( dom t) & k >= kII9 holds (p . (t . k)) = oI;

          let a;

          assume

           A42: a <> b;

          for i holds a <_ ((p . i),b)

          proof

            let i;

            consider k be object such that

             A43: k in ( dom t) and

             A44: i = (t . k) by A25, FUNCT_1:def 3;

            reconsider k as Nat by A43;

            k <= ( len t) by A43, FINSEQ_3: 25;

            then (k + 0 ) < kII9 by XREAL_1: 8;

            then (p . i) = oII by A41, A43, A44;

            hence thesis by A28, A42;

          end;

          hence thesis by A1;

        end;

        then

         A45: ex kII9 be Nat st Q[kII9];

        consider kII be Nat such that

         A46: Q[kII] & for k0 be Nat st Q[k0] holds k0 >= kII from NAT_1:sch 5( A45);

        consider pII such that

         A47: for k st k in ( dom t) & k < kII holds (pII . (t . k)) = oII and

         A48: for k st k in ( dom t) & k >= kII holds (pII . (t . k)) = oI by A29;

        

         A49: kII > 1

        proof

          assume

           A50: kII <= 1;

          consider a such that

           A51: a <> b by A3, Th1, XXREAL_0: 2;

          

           A52: for i holds b <_ ((pII . i),a)

          proof

            let i;

            consider k be object such that

             A53: k in ( dom t) and

             A54: i = (t . k) by A25, FUNCT_1:def 3;

            reconsider k as Nat by A53;

            k >= 1 by A53, FINSEQ_3: 25;

            then (pII . i) = oI by A48, A50, A53, A54, XXREAL_0: 2;

            hence thesis by A27, A51;

          end;

          

           A55: a <_ ((f . pII),b) by A46, A47, A48, A51;

          b <_ ((f . pII),a) by A1, A52;

          hence contradiction by A55, Th4;

        end;

        then

        reconsider kI = (kII - 1) as Nat by NAT_1: 20;

        reconsider kI as Element of NAT by ORDINAL1:def 12;

        

         A56: kII = (kI + 1);

        kI > (1 - 1) by A49, XREAL_1: 9;

        then

         A57: kI >= ( 0 + 1) by INT_1: 7;

        kII <= kII9 by A40, A46;

        then kI <= (kII9 - 1) by XREAL_1: 9;

        then

         A58: kI in ( dom t) by A57, FINSEQ_3: 25;

        then

        reconsider nb = (t . kI) as Element of N by PARTFUN1: 4;

        

         A59: (kI + 0 ) < kII by A56, XREAL_1: 8;

        then

        consider pI such that

         A60: for k st k in ( dom t) & k < kI holds (pI . (t . k)) = oII and

         A61: for k st k in ( dom t) & k >= kI holds (pI . (t . k)) = oI and

         A62: not (for a st a <> b holds a <_ ((f . pI),b)) by A46;

        take nb, pI, pII;

        thus for i st i <> nb holds (pI . i) = (pII . i)

        proof

          let i;

          assume

           A63: i <> nb;

          consider k be object such that

           A64: k in ( dom t) and

           A65: i = (t . k) by A25, FUNCT_1:def 3;

          reconsider k as Nat by A64;

          per cases by A63, A65, XXREAL_0: 1;

            suppose k < kI;

            then (k + 0 ) < kII & (pI . i) = oII by A56, A60, A64, A65, XREAL_1: 8;

            hence thesis by A47, A64, A65;

          end;

            suppose k > kI;

            then k >= kII & (pI . i) = oI by A56, A61, A64, A65, INT_1: 7;

            hence thesis by A48, A64, A65;

          end;

        end;

        thus

         A66: for i holds extreme[(pI . i), b]

        proof

          let i;

          ex k be object st k in ( dom t) & i = (t . k) by A25, FUNCT_1:def 3;

          then (pI . i) = oII or (pI . i) = oI by A60, A61;

          hence thesis by A27, A28;

        end;

        thus for i holds extreme[(pII . i), b]

        proof

          let i;

          ex k be object st k in ( dom t) & i = (t . k) by A25, FUNCT_1:def 3;

          then (pII . i) = oII or (pII . i) = oI by A47, A48;

          hence thesis by A27, A28;

        end;

        (pI . nb) = oI by A58, A61;

        hence for a st a <> b holds b <_ ((pI . nb),a) by A27;

        (pII . nb) = oII by A47, A58, A59;

        hence for a st a <> b holds a <_ ((pII . nb),b) by A28;

        thus for a st a <> b holds b <_ ((f . pI),a) by A4, A62, A66;

        thus thesis by A46, A47, A48;

      end;

      

       A67: for b holds ex nb, pI, pII st (for i st i <> nb holds (pI . i) = (pII . i)) & (for i holds extreme[(pI . i), b]) & (for a st a <> b holds b <_ ((f . pI),a)) & (for a st a <> b holds a <_ ((f . pII),b)) & for p, a, c st a <> b & c <> b & a <_ ((p . nb),c) holds a <_ ((f . p),c)

      proof

        let b;

        consider nb, pI, pII such that

         A68: for i st i <> nb holds (pI . i) = (pII . i) and

         A69: for i holds extreme[(pI . i), b] and

         A70: for i holds extreme[(pII . i), b] and

         A71: for a st a <> b holds b <_ ((pI . nb),a) and

         A72: for a st a <> b holds a <_ ((pII . nb),b) and

         A73: (for a st a <> b holds b <_ ((f . pI),a)) & for a st a <> b holds a <_ ((f . pII),b) by A24;

        take nb, pI, pII;

        thus (for i st i <> nb holds (pI . i) = (pII . i)) & (for i holds extreme[(pI . i), b]) & (for a st a <> b holds b <_ ((f . pI),a)) & for a st a <> b holds a <_ ((f . pII),b) by A68, A69, A73;

        let p, a, c;

        assume that

         A74: a <> b and

         A75: c <> b and

         A76: a <_ ((p . nb),c);

        

         A77: a <> c by A76, Th3;

        defpred P[ Element of N, Element of ( LinPreorders A)] means (a <_ ((p . $1),c) iff a <_ ($2,c)) & (c <_ ((p . $1),a) iff c <_ ($2,a)) & ($1 = nb implies a <_ ($2,b) & b <_ ($2,c)) & ($1 <> nb implies ((for d st d <> b holds b <_ ((pII . $1),d)) implies b <_ ($2,a) & b <_ ($2,c)) & ((for d st d <> b holds d <_ ((pII . $1),b)) implies a <_ ($2,b) & c <_ ($2,b)));

        

         A78: for i holds ex o st P[i, o]

        proof

          let i;

          per cases ;

            suppose

             A79: i = nb;

            consider o such that

             A80: a <_ (o,b) & b <_ (o,c) by A74, A75, A77, Th7;

            take o;

            thus thesis by A76, A79, A80, Th4, Th5;

          end;

            suppose

             A81: i <> nb;

            per cases by A70;

              suppose for d st d <> b holds b <_ ((pII . i),d);

              then b <_ ((pII . i),a) by A74;

              then

               A82: not a <_ ((pII . i),b) by Th4;

              consider o such that

               A83: b <_ (o,a) & b <_ (o,c) & (a <_ (o,c) iff a <_ ((p . i),c)) & (c <_ (o,a) iff c <_ ((p . i),a)) by A74, A75, Th10;

              take o;

              thus thesis by A74, A81, A82, A83;

            end;

              suppose for d st d <> b holds d <_ ((pII . i),b);

              then a <_ ((pII . i),b) by A74;

              then

               A84: not b <_ ((pII . i),a) by Th4;

              consider o such that

               A85: a <_ (o,b) & c <_ (o,b) & (a <_ (o,c) iff a <_ ((p . i),c)) & (c <_ (o,a) iff c <_ ((p . i),a)) by A74, A75, Th11;

              take o;

              thus thesis by A74, A81, A84, A85;

            end;

          end;

        end;

        consider pIII be Function of N, ( LinPreorders A) such that

         A86: for i holds P[i, (pIII . i)] from FUNCT_2:sch 3( A78);

        reconsider pIII as Element of ( Funcs (N,( LinPreorders A))) by FUNCT_2: 8;

        for i holds (a <_ ((pII . i),b) iff a <_ ((pIII . i),b)) & (b <_ ((pII . i),a) iff b <_ ((pIII . i),a))

        proof

          let i;

          per cases ;

            suppose i = nb;

            then a <_ ((pII . i),b) & a <_ ((pIII . i),b) by A72, A74, A86;

            hence thesis by Th4;

          end;

            suppose

             A87: i <> nb;

            per cases by A70;

              suppose for d st d <> b holds b <_ ((pII . i),d);

              then b <_ ((pII . i),a) & b <_ ((pIII . i),a) by A74, A86, A87;

              hence thesis by Th4;

            end;

              suppose for d st d <> b holds d <_ ((pII . i),b);

              then a <_ ((pII . i),b) & a <_ ((pIII . i),b) by A74, A86, A87;

              hence thesis by Th4;

            end;

          end;

        end;

        then

         A88: a <_ ((f . pII),b) iff a <_ ((f . pIII),b) by A2;

        for i holds (b <_ ((pI . i),c) iff b <_ ((pIII . i),c)) & (c <_ ((pI . i),b) iff c <_ ((pIII . i),b))

        proof

          let i;

          per cases ;

            suppose i = nb;

            then b <_ ((pI . i),c) & b <_ ((pIII . i),c) by A71, A75, A86;

            hence thesis by Th4;

          end;

            suppose

             A89: i <> nb;

            per cases by A70;

              suppose

               A90: for d st d <> b holds b <_ ((pII . i),d);

              then b <_ ((pII . i),c) by A75;

              then

               A91: b <_ ((pI . i),c) by A68, A89;

              b <_ ((pIII . i),c) by A86, A89, A90;

              hence thesis by A91, Th4;

            end;

              suppose

               A92: for d st d <> b holds d <_ ((pII . i),b);

              then c <_ ((pII . i),b) by A75;

              then

               A93: c <_ ((pI . i),b) by A68, A89;

              c <_ ((pIII . i),b) by A86, A89, A92;

              hence thesis by A93, Th4;

            end;

          end;

        end;

        then b <_ ((f . pI),c) iff b <_ ((f . pIII),c) by A2;

        then a <_ ((f . pIII),c) by A73, A74, A88, Th5;

        hence thesis by A2, A86;

      end;

      set b = the Element of A;

      consider nb, pI, pII such that

       A94: for i st i <> nb holds (pI . i) = (pII . i) and

       A95: for i holds extreme[(pI . i), b] and

       A96: (for a st a <> b holds b <_ ((f . pI),a)) & for a st a <> b holds a <_ ((f . pII),b) and

       A97: for p, a, c st a <> b & c <> b & a <_ ((p . nb),c) holds a <_ ((f . p),c) by A67;

      take nb;

      let p, a, a9;

      assume

       A98: a <_ ((p . nb),a9);

      then

       A99: a <> a9 by Th4;

      per cases ;

        suppose a <> b & a9 <> b;

        hence thesis by A97, A98;

      end;

        suppose

         A100: a = b or a9 = b;

        consider c such that

         A101: c <> a & c <> a9 by A3, Th2;

        consider nc, pI9, pII9 such that for i st i <> nc holds (pI9 . i) = (pII9 . i) and for i holds extreme[(pI9 . i), c] and for a st a <> c holds c <_ ((f . pI9),a) and for a st a <> c holds a <_ ((f . pII9),c) and

         A102: for p, a, a9 st a <> c & a9 <> c & a <_ ((p . nc),a9) holds a <_ ((f . p),a9) by A67;

        nc = nb

        proof

          per cases by A100;

            suppose

             A103: a = b;

            assume

             A104: nc <> nb;

            b <_ ((pI . nc),a9) or a9 <_ ((pI . nc),b) by A95, A99, A103;

            then b <_ ((pII . nc),a9) & a9 <_ ((f . pII),b) or a9 <_ ((pI . nc),b) & b <_ ((f . pI),a9) by A94, A96, A99, A103, A104;

            then b <_ ((pII . nc),a9) & a9 <=_ ((f . pII),b) or a9 <_ ((pI . nc),b) & b <=_ ((f . pI),a9) by Th4;

            hence contradiction by A101, A102, A103;

          end;

            suppose

             A105: a9 = b;

            assume

             A106: nc <> nb;

            b <_ ((pI . nc),a) or a <_ ((pI . nc),b) by A95, A99, A105;

            then b <_ ((pII . nc),a) & a <_ ((f . pII),b) or a <_ ((pI . nc),b) & b <_ ((f . pI),a) by A94, A96, A99, A105, A106;

            then b <_ ((pII . nc),a) & a <=_ ((f . pII),b) or a <_ ((pI . nc),b) & b <=_ ((f . pI),a) by Th4;

            hence contradiction by A101, A102, A105;

          end;

        end;

        hence thesis by A98, A101, A102;

      end;

    end;

    reserve o,o1 for Element of ( LinOrders A);

    reserve o9 for Element of ( LinPreorders A);

    reserve p,p9 for Element of ( Funcs (N,( LinOrders A)));

    reserve q,q9 for Element of ( Funcs (N,( LinPreorders A)));

    reserve f for Function of ( Funcs (N,( LinOrders A))), ( LinPreorders A);

    theorem :: ARROW:15

    (for p, a, b st for i holds a <_ ((p . i),b) holds a <_ ((f . p),b)) & (for p, p9, a, b st for i holds a <_ ((p . i),b) iff a <_ ((p9 . i),b) holds a <_ ((f . p),b) iff a <_ ((f . p9),b)) & ( card A) >= 3 implies ex n st for p, a, b holds a <_ ((p . n),b) iff a <_ ((f . p),b)

    proof

      assume that

       A1: for p, a, b st for i holds a <_ ((p . i),b) holds a <_ ((f . p),b) and

       A2: for p, p9, a, b st for i holds a <_ ((p . i),b) iff a <_ ((p9 . i),b) holds a <_ ((f . p),b) iff a <_ ((f . p9),b) and

       A3: ( card A) >= 3;

      set o = the Element of ( LinOrders A);

      defpred O[ Element of ( LinPreorders A), Element of A, Element of A] means $2 <=_ ($1,$3) & ($2 <_ ($1,$3) or $2 <=_ (o,$3));

      defpred P[ Element of ( LinPreorders A), Element of ( LinOrders A)] means for a, b holds O[$1, a, b] iff a <=_ ($2,b);

      

       A4: for o9 holds ex o1 st P[o9, o1]

      proof

        let o9;

        defpred Q[ Element of A, Element of A] means O[o9, $1, $2];

        consider o1 be Relation of A such that

         A5: for a, b holds [a, b] in o1 iff Q[a, b] from RELSET_1:sch 2;

         A6:

        now

          let a, b;

           Q[a, b] or Q[b, a] by Th4;

          hence [a, b] in o1 or [b, a] in o1 by A5;

        end;

        now

          let a, b, c;

           Q[a, b] & Q[b, c] implies Q[a, c] by Th5;

          hence [a, b] in o1 & [b, c] in o1 implies [a, c] in o1 by A5;

        end;

        then

        reconsider o1 as Element of ( LinPreorders A) by A6, Def1;

        now

          let a, b;

           Q[a, b] & Q[b, a] implies a = b by Th6;

          hence [a, b] in o1 & [b, a] in o1 implies a = b by A5;

        end;

        then

        reconsider o1 as Element of ( LinOrders A) by Def2;

        take o1;

        let a, b;

         [a, b] in o1 iff Q[a, b] by A5;

        hence thesis;

      end;

      defpred R[ Element of ( Funcs (N,( LinPreorders A))), Element of ( Funcs (N,( LinOrders A)))] means for i holds P[($1 . i), ($2 . i)];

      

       A7: for q, p, p9 st R[q, p] & R[q, p9] holds p = p9

      proof

        let q, p, p9;

        assume that

         A8: R[q, p] and

         A9: R[q, p9];

        let i;

        reconsider pi = (p . i) as Relation of A by Def1;

        reconsider pi9 = (p9 . i) as Relation of A by Def1;

        now

          let a, b;

          

           A10: O[(q . i), a, b] iff a <=_ ((p . i),b) by A8;

           O[(q . i), a, b] iff a <=_ ((p9 . i),b) by A9;

          hence [a, b] in (p . i) iff [a, b] in (p9 . i) by A10;

        end;

        then pi = pi9 by RELSET_1:def 2;

        hence (p . i) = (p9 . i);

      end;

      

       A11: for q holds ex p st R[q, p]

      proof

        let q;

        defpred S[ Element of N, Element of ( LinOrders A)] means P[(q . $1), $2];

        

         A12: for i holds ex o1 st S[i, o1] by A4;

        consider p be Function of N, ( LinOrders A) such that

         A13: for i holds S[i, (p . i) qua Element of ( LinOrders A)] from FUNCT_2:sch 3( A12);

        reconsider p as Element of ( Funcs (N,( LinOrders A))) by FUNCT_2: 8;

        take p;

        thus thesis by A13;

      end;

      defpred T[ Element of ( Funcs (N,( LinPreorders A))), Element of ( LinPreorders A)] means ex p st R[$1, p] & (f . p) = $2;

      

       A14: for q holds ex o9 st T[q, o9]

      proof

        let q;

        consider p such that

         A15: R[q, p] by A11;

        take (f . p);

        thus thesis by A15;

      end;

      consider f9 be Function of ( Funcs (N,( LinPreorders A))), ( LinPreorders A) such that

       A16: for q holds T[q, (f9 . q)] from FUNCT_2:sch 3( A14);

      

       A17: for q, a, b st for i holds a <_ ((q . i),b) holds a <_ ((f9 . q),b)

      proof

        let q, a, b;

        assume

         A18: for i holds a <_ ((q . i),b);

        consider p such that

         A19: R[q, p] and

         A20: (f . p) = (f9 . q) by A16;

        now

          let i;

           not O[(q . i), b, a] by A18;

          hence a <_ ((p . i),b) by A19;

        end;

        hence thesis by A1, A20;

      end;

      now

        let q, q9, a, b;

        assume

         A21: for i holds (a <_ ((q . i),b) iff a <_ ((q9 . i),b)) & (b <_ ((q . i),a) iff b <_ ((q9 . i),a));

        consider p such that

         A22: R[q, p] and

         A23: (f . p) = (f9 . q) by A16;

        consider p9 such that

         A24: R[q9, p9] and

         A25: (f . p9) = (f9 . q9) by A16;

        for i holds a <_ ((p . i),b) iff a <_ ((p9 . i),b)

        proof

          let i;

           O[(q . i), b, a] iff O[(q9 . i), b, a] by A21;

          hence thesis by A22, A24;

        end;

        hence a <_ ((f9 . q),b) iff a <_ ((f9 . q9),b) by A2, A23, A25;

      end;

      then

      consider n such that

       A26: for q, a, b st a <_ ((q . n),b) holds a <_ ((f9 . q),b) by A3, A17, Th14;

      take n;

      let p;

      now

        ( rng p) c= ( LinOrders A) by RELAT_1:def 19;

        then ( dom p) = N & ( rng p) c= ( LinPreorders A) by FUNCT_2:def 1, XBOOLE_1: 1;

        then

        reconsider q = p as Element of ( Funcs (N,( LinPreorders A))) by FUNCT_2:def 2;

        

         A27: R[q, p]

        proof

          let i;

          let a, b;

          a <_ ((p . i),b) or a = b or a >_ ((p . i),b) by Th6;

          hence thesis by Th4;

        end;

        

         A28: ex p9 st R[q, p9] & (f . p9) = (f9 . q) by A16;

        let a, b;

        assume a <_ ((p . n),b);

        then a <_ ((f9 . q),b) by A26;

        hence a <_ ((f . p),b) by A7, A27, A28;

      end;

      hence thesis by Th13;

    end;