eqrel_1.miz



    begin

    reserve X,Y,Z for set,

x,y,z for object;

    reserve i,j for Nat;

    reserve A,B,C for Subset of X;

    reserve R,R1,R2 for Relation of X;

    reserve AX for Subset of [:X, X:];

    reserve SFXX for Subset-Family of [:X, X:];

    definition

      let X;

      :: EQREL_1:def1

      func nabla X -> Relation of X equals [:X, X:];

      coherence

      proof

         [:X, X:] c= [:X, X:];

        hence thesis;

      end;

    end

    registration

      let X;

      cluster ( nabla X) -> total reflexive;

      coherence

      proof

        thus ( dom ( nabla X)) c= X;

        thus X c= ( dom ( nabla X))

        proof

          let x be object;

          assume x in X;

          then [x, x] in [:X, X:] by ZFMISC_1: 87;

          hence thesis by XTUPLE_0:def 12;

        end;

        let x be object;

        assume x in ( field ( nabla X));

        then x in (( dom ( nabla X)) \/ ( rng ( nabla X)));

        hence thesis by ZFMISC_1: 87;

      end;

    end

    definition

      let X, R1, R2;

      :: original: /\

      redefine

      func R1 /\ R2 -> Relation of X ;

      coherence

      proof

        (R1 /\ R2) c= [:X, X:];

        hence thesis;

      end;

      :: original: \/

      redefine

      func R1 \/ R2 -> Relation of X ;

      coherence

      proof

        (R1 \/ R2) c= [:X, X:];

        hence thesis;

      end;

    end

    theorem :: EQREL_1:1

    (( nabla X) \/ R1) = ( nabla X) by XBOOLE_1: 12;

    theorem :: EQREL_1:2

    ( id X) is_reflexive_in X & ( id X) is_symmetric_in X & ( id X) is_transitive_in X by RELAT_1:def 10;

    definition

      let X;

      mode Tolerance of X is total reflexive symmetric Relation of X;

      mode Equivalence_Relation of X is total symmetric transitive Relation of X;

    end

    theorem :: EQREL_1:3

    ( id X) is Equivalence_Relation of X;

    theorem :: EQREL_1:4

    

     Th4: ( nabla X) is Equivalence_Relation of X

    proof

      for x, y holds x in X & y in X & [x, y] in ( nabla X) implies [y, x] in ( nabla X) by ZFMISC_1: 88;

      then

       A1: ( nabla X) is_symmetric_in X;

      for x, y, z st x in X & y in X & z in X & [x, y] in ( nabla X) & [y, z] in ( nabla X) holds [x, z] in ( nabla X) by ZFMISC_1: 87;

      then

       A2: ( nabla X) is_transitive_in X;

      ( field ( nabla X)) = X by ORDERS_1: 12;

      hence thesis by A1, A2, RELAT_2:def 11, RELAT_2:def 16;

    end;

    registration

      let X;

      cluster ( nabla X) -> total symmetric transitive;

      coherence by Th4;

    end

    reserve EqR,EqR1,EqR2,EqR3 for Equivalence_Relation of X;

    

     Lm1: [x, y] in R implies x in X & y in X

    proof

      assume [x, y] in R;

      then x in ( dom R) & y in ( rng R) by XTUPLE_0:def 12, XTUPLE_0:def 13;

      hence thesis;

    end;

    theorem :: EQREL_1:5

    

     Th5: for R be total reflexive Relation of X holds x in X implies [x, x] in R

    proof

      let R be total reflexive Relation of X;

      ( field R) = X by ORDERS_1: 12;

      then R is_reflexive_in X by RELAT_2:def 9;

      hence thesis;

    end;

    theorem :: EQREL_1:6

    

     Th6: for X be set, x,y be object, R be symmetric Relation of X st [x, y] in R holds [y, x] in R

    proof

      let X be set, x,y be object, R be symmetric Relation of X;

      assume

       A1: [x, y] in R;

      then x in ( field R) & y in ( field R) by RELAT_1: 15;

      hence thesis by A1, RELAT_2:def 3, RELAT_2:def 11;

    end;

    theorem :: EQREL_1:7

    

     Th7: for R be total transitive Relation of X holds for x,y be object holds [x, y] in R & [y, z] in R implies [x, z] in R

    proof

      let R be total transitive Relation of X;

      let x,y be object;

      assume that

       A1: [x, y] in R and

       A2: [y, z] in R;

      

       A3: z in X by A2, Lm1;

      ( field R) = X by ORDERS_1: 12;

      then

       A4: R is_transitive_in X by RELAT_2:def 16;

      x in X & y in X by A1, Lm1;

      hence thesis by A1, A2, A3, A4;

    end;

    theorem :: EQREL_1:8

    for R be total reflexive Relation of X holds (ex x be set st x in X) implies R <> {} ;

    theorem :: EQREL_1:9

    

     Th9: R is Equivalence_Relation of X iff R is reflexive symmetric transitive & ( field R) = X by ORDERS_1: 12, ORDERS_1: 13, PARTFUN1:def 2;

    definition

      let X, EqR1, EqR2;

      :: original: /\

      redefine

      func EqR1 /\ EqR2 -> Equivalence_Relation of X ;

      coherence

      proof

        for x be object st x in X holds [x, x] in EqR2 by Th5;

        then

         A1: ( id X) c= EqR2 by RELAT_1: 47;

        for x be object st x in X holds [x, x] in EqR1 by Th5;

        then ( id X) c= EqR1 by RELAT_1: 47;

        then ( id X) c= (EqR1 /\ EqR2) by A1, XBOOLE_1: 19;

        then ( dom (EqR1 /\ EqR2)) = X & ( rng (EqR1 /\ EqR2)) = X by RELSET_1: 16;

        then ( field (EqR1 /\ EqR2)) = X;

        hence thesis by Th9;

      end;

    end

    theorem :: EQREL_1:10

    (( id X) /\ EqR) = ( id X)

    proof

      now

        let x,y be object;

        assume [x, y] in ( id X);

        then x in X & x = y by RELAT_1:def 10;

        hence [x, y] in EqR by Th5;

      end;

      then ( id X) c= EqR;

      hence thesis by XBOOLE_1: 28;

    end;

    theorem :: EQREL_1:11

    

     Th11: for SFXX st (SFXX <> {} & for Y st Y in SFXX holds Y is Equivalence_Relation of X) holds ( meet SFXX) is Equivalence_Relation of X

    proof

      let SFXX such that

       A1: SFXX <> {} and

       A2: for Y st Y in SFXX holds Y is Equivalence_Relation of X;

      reconsider XX = ( meet SFXX) as Relation of X;

      

       A3: XX is_symmetric_in X

      proof

        let x, y;

        assume that x in X and y in X and

         A4: [x, y] in XX;

        now

          let Y;

          assume Y in SFXX;

          then Y is Equivalence_Relation of X & [x, y] in Y by A2, A4, SETFAM_1:def 1;

          hence [y, x] in Y by Th6;

        end;

        hence thesis by A1, SETFAM_1:def 1;

      end;

      

       A5: XX is_transitive_in X

      proof

        let x, y, z;

        assume that x in X and y in X and z in X and

         A6: [x, y] in XX and

         A7: [y, z] in XX;

        now

          let Y;

          assume

           A8: Y in SFXX;

          then

           A9: [y, z] in Y by A7, SETFAM_1:def 1;

          Y is Equivalence_Relation of X & [x, y] in Y by A2, A6, A8, SETFAM_1:def 1;

          hence [x, z] in Y by A9, Th7;

        end;

        hence thesis by A1, SETFAM_1:def 1;

      end;

      XX is_reflexive_in X

      proof

        let x such that

         A10: x in X;

        for Y st Y in SFXX holds [x, x] in Y

        proof

          let Y;

          assume Y in SFXX;

          then Y is Equivalence_Relation of X by A2;

          hence thesis by A10, Th5;

        end;

        hence thesis by A1, SETFAM_1:def 1;

      end;

      then ( field XX) = X & ( dom XX) = X by ORDERS_1: 13;

      hence thesis by A3, A5, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16;

    end;

    theorem :: EQREL_1:12

    

     Th12: for R holds ex EqR st R c= EqR & for EqR2 st R c= EqR2 holds EqR c= EqR2

    proof

      let R;

      defpred P[ set] means $1 is Equivalence_Relation of X & R c= $1;

      consider F be Subset-Family of [:X, X:] such that

       A1: for AX holds AX in F iff P[AX] from SUBSET_1:sch 3;

      R c= ( nabla X);

      then

       A2: F <> {} by A1;

      for Y st Y in F holds Y is Equivalence_Relation of X by A1;

      then

      reconsider EqR = ( meet F) as Equivalence_Relation of X by A2, Th11;

      

       A3: for EqR2 st R c= EqR2 holds EqR c= EqR2 by A1, SETFAM_1: 3;

      take EqR;

      for Y st Y in F holds R c= Y by A1;

      hence thesis by A2, A3, SETFAM_1: 5;

    end;

    definition

      let X;

      let EqR1, EqR2;

      :: EQREL_1:def2

      func EqR1 "\/" EqR2 -> Equivalence_Relation of X means

      : Def2: (EqR1 \/ EqR2) c= it & for EqR st (EqR1 \/ EqR2) c= EqR holds it c= EqR;

      existence by Th12;

      uniqueness ;

      commutativity ;

      idempotence ;

    end

    theorem :: EQREL_1:13

    ((EqR1 "\/" EqR2) "\/" EqR3) = (EqR1 "\/" (EqR2 "\/" EqR3))

    proof

      for EqR4 be Equivalence_Relation of X holds EqR4 = (EqR1 "\/" (EqR2 "\/" EqR3)) implies ((EqR1 "\/" EqR2) "\/" EqR3) c= EqR4

      proof

        let EqR4 be Equivalence_Relation of X;

        

         A1: (EqR2 \/ EqR3) c= (EqR2 "\/" EqR3) by Def2;

        assume EqR4 = (EqR1 "\/" (EqR2 "\/" EqR3));

        then

         A2: (EqR1 \/ (EqR2 "\/" EqR3)) c= EqR4 by Def2;

        (EqR2 "\/" EqR3) c= (EqR1 \/ (EqR2 "\/" EqR3)) by XBOOLE_1: 7;

        then (EqR2 "\/" EqR3) c= EqR4 by A2;

        then

         A3: (EqR2 \/ EqR3) c= EqR4 by A1;

        EqR2 c= (EqR2 \/ EqR3) by XBOOLE_1: 7;

        then

         A4: EqR2 c= EqR4 by A3;

        EqR1 c= (EqR1 \/ (EqR2 "\/" EqR3)) by XBOOLE_1: 7;

        then EqR1 c= EqR4 by A2;

        then (EqR1 \/ EqR2) c= EqR4 by A4, XBOOLE_1: 8;

        then

         A5: (EqR1 "\/" EqR2) c= EqR4 by Def2;

        EqR3 c= (EqR2 \/ EqR3) by XBOOLE_1: 7;

        then EqR3 c= EqR4 by A3;

        then ((EqR1 "\/" EqR2) \/ EqR3) c= EqR4 by A5, XBOOLE_1: 8;

        hence thesis by Def2;

      end;

      then

       A6: ((EqR1 "\/" EqR2) "\/" EqR3) c= (EqR1 "\/" (EqR2 "\/" EqR3));

      for EqR4 be Equivalence_Relation of X holds EqR4 = ((EqR1 "\/" EqR2) "\/" EqR3) implies (EqR1 "\/" (EqR2 "\/" EqR3)) c= EqR4

      proof

        let EqR4 be Equivalence_Relation of X;

        

         A7: (EqR1 \/ EqR2) c= (EqR1 "\/" EqR2) by Def2;

        assume EqR4 = ((EqR1 "\/" EqR2) "\/" EqR3);

        then

         A8: ((EqR1 "\/" EqR2) \/ EqR3) c= EqR4 by Def2;

        (EqR1 "\/" EqR2) c= ((EqR1 "\/" EqR2) \/ EqR3) by XBOOLE_1: 7;

        then (EqR1 "\/" EqR2) c= EqR4 by A8;

        then

         A9: (EqR1 \/ EqR2) c= EqR4 by A7;

        EqR3 c= ((EqR1 "\/" EqR2) \/ EqR3) by XBOOLE_1: 7;

        then

         A10: EqR3 c= EqR4 by A8;

        EqR2 c= (EqR1 \/ EqR2) by XBOOLE_1: 7;

        then EqR2 c= EqR4 by A9;

        then (EqR2 \/ EqR3) c= EqR4 by A10, XBOOLE_1: 8;

        then

         A11: (EqR2 "\/" EqR3) c= EqR4 by Def2;

        EqR1 c= (EqR1 \/ EqR2) by XBOOLE_1: 7;

        then EqR1 c= EqR4 by A9;

        then (EqR1 \/ (EqR2 "\/" EqR3)) c= EqR4 by A11, XBOOLE_1: 8;

        hence thesis by Def2;

      end;

      then (EqR1 "\/" (EqR2 "\/" EqR3)) c= ((EqR1 "\/" EqR2) "\/" EqR3);

      hence thesis by A6;

    end;

    theorem :: EQREL_1:14

    (EqR "\/" EqR) = EqR;

    theorem :: EQREL_1:15

    (EqR1 "\/" EqR2) = (EqR2 "\/" EqR1);

    theorem :: EQREL_1:16

    (EqR1 /\ (EqR1 "\/" EqR2)) = EqR1

    proof

      thus (EqR1 /\ (EqR1 "\/" EqR2)) c= EqR1 by XBOOLE_1: 17;

      EqR1 c= (EqR1 \/ EqR2) & (EqR1 \/ EqR2) c= (EqR1 "\/" EqR2) by Def2, XBOOLE_1: 7;

      then EqR1 c= (EqR1 "\/" EqR2);

      hence thesis by XBOOLE_1: 19;

    end;

    theorem :: EQREL_1:17

    (EqR1 "\/" (EqR1 /\ EqR2)) = EqR1

    proof

      EqR1 = (EqR1 \/ (EqR1 /\ EqR2)) & for EqR st (EqR1 \/ (EqR1 /\ EqR2)) c= EqR holds EqR1 c= EqR by XBOOLE_1: 22;

      hence thesis by Def2;

    end;

    scheme :: EQREL_1:sch1

    ExEqRel { X() -> set , P[ object, object] } :

ex EqR be Equivalence_Relation of X() st for x, y holds [x, y] in EqR iff x in X() & y in X() & P[x, y]

      provided

       A1: for x st x in X() holds P[x, x]

       and

       A2: for x, y st P[x, y] holds P[y, x]

       and

       A3: for x, y, z st P[x, y] & P[y, z] holds P[x, z];

      consider Y be Relation of X(), X() such that

       A4: for x, y holds [x, y] in Y iff x in X() & y in X() & P[x, y] from RELSET_1:sch 1;

      

       A5: Y is_transitive_in X()

      proof

        let x, y, z;

        assume that

         A6: x in X() and y in X() and

         A7: z in X() and

         A8: [x, y] in Y & [y, z] in Y;

        P[x, y] & P[y, z] by A4, A8;

        then P[x, z] by A3;

        hence thesis by A4, A6, A7;

      end;

      

       A9: Y is_symmetric_in X()

      proof

        let x, y;

        assume that

         A10: x in X() & y in X() and

         A11: [x, y] in Y;

        P[x, y] by A4, A11;

        then P[y, x] by A2;

        hence thesis by A4, A10;

      end;

      Y is_reflexive_in X() by A1, A4;

      then ( field Y) = X() & ( dom Y) = X() by ORDERS_1: 13;

      then

      reconsider R1 = Y as Equivalence_Relation of X() by A9, A5, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16;

      take R1;

      thus thesis by A4;

    end;

    notation

      let R be Relation, x be object;

      synonym Class (R,x) for Im (R,x);

    end

    definition

      let X,Y be set, R be Relation of X, Y, x be object;

      :: original: Class

      redefine

      func Class (R,x) -> Subset of Y ;

      coherence

      proof

        (R .: {x}) c= Y;

        hence thesis;

      end;

    end

    theorem :: EQREL_1:18

    for R be Relation holds y in ( Class (R,x)) iff [x, y] in R

    proof

      let R be Relation;

      thus y in ( Class (R,x)) implies [x, y] in R

      proof

        assume y in ( Class (R,x));

        then ex z be object st [z, y] in R & z in {x} by RELAT_1:def 13;

        hence thesis by TARSKI:def 1;

      end;

      

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

      assume [x, y] in R;

      hence thesis by A1, RELAT_1:def 13;

    end;

    theorem :: EQREL_1:19

    

     Th19: for R be total symmetric Relation of X holds y in ( Class (R,x)) iff [y, x] in R

    proof

      let R be total symmetric Relation of X;

      thus y in ( Class (R,x)) implies [y, x] in R

      proof

        assume y in ( Class (R,x));

        then ex z be object st [z, y] in R & z in {x} by RELAT_1:def 13;

        then [x, y] in R by TARSKI:def 1;

        hence thesis by Th6;

      end;

      assume [y, x] in R;

      then

       A1: [x, y] in R by Th6;

      x in {x} by TARSKI:def 1;

      hence thesis by A1, RELAT_1:def 13;

    end;

    theorem :: EQREL_1:20

    

     Th20: for R be Tolerance of X holds for x st x in X holds x in ( Class (R,x))

    proof

      let R be Tolerance of X;

      let x;

      assume x in X;

      then [x, x] in R by Th5;

      hence thesis by Th19;

    end;

    theorem :: EQREL_1:21

    for R be Tolerance of X holds for x st x in X holds ex y st x in ( Class (R,y))

    proof

      let R be Tolerance of X;

      let x;

      assume x in X;

      then x in ( Class (R,x)) by Th20;

      hence thesis;

    end;

    theorem :: EQREL_1:22

    for R be transitive Tolerance of X holds y in ( Class (R,x)) & z in ( Class (R,x)) implies [y, z] in R

    proof

      let R be transitive Tolerance of X;

      assume that

       A1: y in ( Class (R,x)) and

       A2: z in ( Class (R,x));

       [z, x] in R by A2, Th19;

      then

       A3: [x, z] in R by Th6;

       [y, x] in R by A1, Th19;

      hence thesis by A3, Th7;

    end;

    

     Lm2: for x st x in X holds [x, y] in EqR iff ( Class (EqR,x)) = ( Class (EqR,y))

    proof

      let x such that

       A1: x in X;

      thus [x, y] in EqR implies ( Class (EqR,x)) = ( Class (EqR,y))

      proof

        assume

         A2: [x, y] in EqR;

        now

          let z be object;

          assume z in ( Class (EqR,y));

          then

           A3: [z, y] in EqR by Th19;

           [y, x] in EqR by A2, Th6;

          then [z, x] in EqR by A3, Th7;

          hence z in ( Class (EqR,x)) by Th19;

        end;

        then

         A4: ( Class (EqR,y)) c= ( Class (EqR,x));

        now

          let z be object;

          assume z in ( Class (EqR,x));

          then [z, x] in EqR by Th19;

          then [z, y] in EqR by A2, Th7;

          hence z in ( Class (EqR,y)) by Th19;

        end;

        then ( Class (EqR,x)) c= ( Class (EqR,y));

        hence thesis by A4;

      end;

      assume ( Class (EqR,x)) = ( Class (EqR,y));

      then x in ( Class (EqR,y)) by A1, Th20;

      hence thesis by Th19;

    end;

    theorem :: EQREL_1:23

    

     Th23: for x st x in X holds y in ( Class (EqR,x)) iff ( Class (EqR,x)) = ( Class (EqR,y))

    proof

      let x such that

       A1: x in X;

      thus y in ( Class (EqR,x)) implies ( Class (EqR,x)) = ( Class (EqR,y))

      proof

        assume y in ( Class (EqR,x));

        then [y, x] in EqR by Th19;

        then [x, y] in EqR by Th6;

        hence thesis by A1, Lm2;

      end;

      assume ( Class (EqR,x)) = ( Class (EqR,y));

      then [x, y] in EqR by A1, Lm2;

      then [y, x] in EqR by Th6;

      hence thesis by Th19;

    end;

    theorem :: EQREL_1:24

    

     Th24: for x, y st y in X holds ( Class (EqR,x)) = ( Class (EqR,y)) or ( Class (EqR,x)) misses ( Class (EqR,y))

    proof

      let x, y;

      

       A1: not [x, y] in EqR implies ( Class (EqR,x)) misses ( Class (EqR,y))

      proof

        assume

         A2: not [x, y] in EqR;

        assume ( Class (EqR,x)) meets ( Class (EqR,y));

        then

        consider z be object such that

         A3: z in ( Class (EqR,x)) and

         A4: z in ( Class (EqR,y)) by XBOOLE_0: 3;

         [z, x] in EqR by A3, Th19;

        then

         A5: [x, z] in EqR by Th6;

         [z, y] in EqR by A4, Th19;

        hence contradiction by A2, A5, Th7;

      end;

      assume

       A6: y in X;

       [x, y] in EqR implies ( Class (EqR,x)) = ( Class (EqR,y))

      proof

        assume [x, y] in EqR;

        then x in ( Class (EqR,y)) by Th19;

        hence thesis by A6, Th23;

      end;

      hence thesis by A1;

    end;

    theorem :: EQREL_1:25

    

     Th25: for x st x in X holds ( Class (( id X),x)) = {x}

    proof

      let x;

       A1:

      now

        let y;

        assume y in ( Class (( id X),x));

        then [y, x] in ( id X) by Th19;

        hence y = x by RELAT_1:def 10;

      end;

      assume x in X;

      then for y be object holds y in ( Class (( id X),x)) iff y = x by A1, Th20;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: EQREL_1:26

    

     Th26: for x st x in X holds ( Class (( nabla X),x)) = X

    proof

      let x such that

       A1: x in X;

      now

        let y be object;

        assume y in X;

        then [y, x] in ( nabla X) by A1, ZFMISC_1: 87;

        hence y in ( Class (( nabla X),x)) by Th19;

      end;

      then for y be object holds y in X iff y in ( Class (( nabla X),x));

      hence thesis by TARSKI: 2;

    end;

    theorem :: EQREL_1:27

    

     Th27: (ex x st ( Class (EqR,x)) = X) implies EqR = ( nabla X)

    proof

      given x such that

       A1: ( Class (EqR,x)) = X;

       [:X, X:] c= EqR

      proof

        let y,z be object;

        assume

         A2: [y, z] in [:X, X:];

        then z in ( Class (EqR,x)) by A1, ZFMISC_1: 87;

        then [z, x] in EqR by Th19;

        then

         A3: [x, z] in EqR by Th6;

        y in ( Class (EqR,x)) by A1, A2, ZFMISC_1: 87;

        then [y, x] in EqR by Th19;

        hence thesis by A3, Th7;

      end;

      hence thesis;

    end;

    theorem :: EQREL_1:28

    x in X implies ( [x, y] in (EqR1 "\/" EqR2) iff ex f be FinSequence st 1 <= ( len f) & x = (f . 1) & y = (f . ( len f)) & for i st 1 <= i & i < ( len f) holds [(f . i), (f . (i + 1))] in (EqR1 \/ EqR2))

    proof

      assume

       A1: x in X;

      thus [x, y] in (EqR1 "\/" EqR2) implies ex f be FinSequence st 1 <= ( len f) & x = (f . 1) & y = (f . ( len f)) & for i st 1 <= i & i < ( len f) holds [(f . i), (f . (i + 1))] in (EqR1 \/ EqR2)

      proof

        defpred P[ object, object] means ex f be FinSequence st (1 <= ( len f) & $1 = (f . 1) & $2 = (f . ( len f)) & for i st 1 <= i & i < ( len f) holds [(f . i), (f . (i + 1))] in (EqR1 \/ EqR2));

        consider Y be Relation of X, X such that

         A2: for x, y holds [x, y] in Y iff x in X & y in X & P[x, y] from RELSET_1:sch 1;

        

         A3: Y is_transitive_in X

        proof

          let x, y, z;

          assume that

           A4: x in X and

           A5: y in X and

           A6: z in X and

           A7: [x, y] in Y and

           A8: [y, z] in Y;

          consider g be FinSequence such that

           A9: 1 <= ( len g) and

           A10: y = (g . 1) and

           A11: z = (g . ( len g)) and

           A12: for i st 1 <= i & i < ( len g) holds [(g . i), (g . (i + 1))] in (EqR1 \/ EqR2) by A2, A8;

          consider f be FinSequence such that

           A13: 1 <= ( len f) and

           A14: x = (f . 1) and

           A15: y = (f . ( len f)) and

           A16: for i st 1 <= i & i < ( len f) holds [(f . i), (f . (i + 1))] in (EqR1 \/ EqR2) by A2, A7;

          set h = (f ^ g);

          

           A17: ( len h) = (( len f) + ( len g)) by FINSEQ_1: 22;

          

           A18: (( len f) + 1) <= (( len f) + ( len g)) by A9, XREAL_1: 7;

          

          then

           A19: (h . ( len h)) = (g . ((( len g) + ( len f)) - ( len f))) by A17, FINSEQ_1: 23

          .= (g . ( len g));

          

           A20: for i st 1 <= i & i < ( len h) holds [(h . i), (h . (i + 1))] in (EqR1 \/ EqR2)

          proof

            let i;

            assume that

             A21: 1 <= i and

             A22: i < ( len h);

            

             A23: 1 <= i & i < ( len f) or i = ( len f) or ( len f) < i by A21, XXREAL_0: 1;

            now

              per cases by A22, A23, NAT_1: 13;

                suppose

                 A24: 1 <= i & i < ( len f);

                then 1 <= (i + 1) & (i + 1) <= ( len f) by NAT_1: 13;

                then (i + 1) in ( Seg ( len f)) by FINSEQ_1: 1;

                then (i + 1) in ( dom f) by FINSEQ_1:def 3;

                then

                 A25: (h . (i + 1)) = (f . (i + 1)) by FINSEQ_1:def 7;

                i in ( Seg ( len f)) by A24, FINSEQ_1: 1;

                then i in ( dom f) by FINSEQ_1:def 3;

                then (h . i) = (f . i) by FINSEQ_1:def 7;

                hence thesis by A16, A24, A25;

              end;

                suppose

                 A26: i = ( len f);

                ( len f) in ( Seg ( len f)) by A13, FINSEQ_1: 1;

                then ( len f) in ( dom f) by FINSEQ_1:def 3;

                then

                 A27: (h . i) = y by A15, A26, FINSEQ_1:def 7;

                

                 A28: [y, y] in EqR1 by A5, Th5;

                (h . (i + 1)) = (g . ((1 + ( len f)) - ( len f))) by A18, A26, FINSEQ_1: 23

                .= y by A10;

                hence thesis by A27, A28, XBOOLE_0:def 3;

              end;

                suppose

                 A29: (( len f) + 1) <= i & i < ( len h);

                then ( len f) < i by NAT_1: 13;

                then

                reconsider k = (i - ( len f)) as Element of NAT by NAT_1: 21;

                i < (( len f) + ( len g)) by A29, FINSEQ_1: 22;

                then

                 A30: (i - ( len f)) < ( len g) by XREAL_1: 19;

                (( len f) + 1) <= (i + 1) & (i + 1) <= (( len f) + ( len g)) by A17, A29, NAT_1: 13;

                

                then

                 A31: (h . (i + 1)) = (g . ((1 + i) - ( len f))) by FINSEQ_1: 23

                .= (g . ((i - ( len f)) + 1));

                ((1 + ( len f)) - ( len f)) <= (i - ( len f)) by A29, XREAL_1: 9;

                then [(g . k), (g . (k + 1))] in (EqR1 \/ EqR2) by A12, A30;

                hence thesis by A17, A29, A31, FINSEQ_1: 23;

              end;

            end;

            hence thesis;

          end;

          1 in ( Seg ( len f)) by A13, FINSEQ_1: 1;

          then 1 in ( dom f) by FINSEQ_1:def 3;

          then

           A32: x = (h . 1) by A14, FINSEQ_1:def 7;

          1 <= ( len h) by A13, A17, NAT_1: 12;

          hence thesis by A2, A4, A6, A11, A32, A19, A20;

        end;

        

         A33: Y is_symmetric_in X

        proof

          let x, y;

          assume that

           A34: x in X & y in X and

           A35: [x, y] in Y;

          consider f be FinSequence such that

           A36: 1 <= ( len f) and

           A37: x = (f . 1) and

           A38: y = (f . ( len f)) and

           A39: for i st 1 <= i & i < ( len f) holds [(f . i), (f . (i + 1))] in (EqR1 \/ EqR2) by A2, A35;

          defpred P[ Nat, object] means $2 = (f . ((1 + ( len f)) - $1));

          

           A40: for k be Nat st k in ( Seg ( len f)) holds ex z be object st P[k, z];

          consider g be FinSequence such that

           A41: ( dom g) = ( Seg ( len f)) & for k be Nat st k in ( Seg ( len f)) holds P[k, (g . k)] from FINSEQ_1:sch 1( A40);

          

           A42: ( len f) = ( len g) by A41, FINSEQ_1:def 3;

          

           A43: for j st 1 <= j & j < ( len g) holds [(g . j), (g . (j + 1))] in (EqR1 \/ EqR2)

          proof

            let j;

            assume that

             A44: 1 <= j and

             A45: j < ( len g);

            reconsider k = (( len f) - j) as Element of NAT by A42, A45, NAT_1: 21;

            (j - ( len f)) < (( len f) - ( len f)) by A42, A45, XREAL_1: 9;

            then ( - (( len f) - j)) < ( - 0 );

            then 0 < k;

            then

             A46: ( 0 + 1) <= k by NAT_1: 13;

            ( - j) < ( - 0 ) by A44, XREAL_1: 24;

            then (( len f) + ( - j)) < ( 0 + ( len f)) by XREAL_1: 6;

            then

             A47: [(f . k), (f . (k + 1))] in (EqR1 \/ EqR2) by A39, A46;

             A48:

            now

              per cases by A47, XBOOLE_0:def 3;

                suppose [(f . k), (f . (k + 1))] in EqR1;

                then [(f . (k + 1)), (f . k)] in EqR1 by Th6;

                hence [(f . (k + 1)), (f . k)] in (EqR1 \/ EqR2) by XBOOLE_0:def 3;

              end;

                suppose [(f . k), (f . (k + 1))] in EqR2;

                then [(f . (k + 1)), (f . k)] in EqR2 by Th6;

                hence [(f . (k + 1)), (f . k)] in (EqR1 \/ EqR2) by XBOOLE_0:def 3;

              end;

            end;

            1 <= (j + 1) & (j + 1) <= ( len f) by A42, A45, NAT_1: 12, NAT_1: 13;

            then (j + 1) in ( Seg ( len f)) by FINSEQ_1: 1;

            

            then

             A49: (g . (j + 1)) = (f . ((( len f) + 1) - (1 + j))) by A41

            .= (f . (( len f) - j));

            j in ( Seg ( len f)) by A42, A44, A45, FINSEQ_1: 1;

            

            then (g . j) = (f . ((1 + ( len f)) - j)) by A41

            .= (f . ((( len f) - j) + 1));

            hence thesis by A49, A48;

          end;

          ( len f) in ( Seg ( len f)) by A36, FINSEQ_1: 1;

          

          then (g . ( len f)) = (f . ((1 + ( len f)) - ( len f))) by A41

          .= (f . (1 + 0 ));

          then

           A50: x = (g . ( len g)) by A37, A41, FINSEQ_1:def 3;

          1 in ( Seg ( len f)) by A36, FINSEQ_1: 1;

          

          then

           A51: (g . 1) = (f . ((( len f) + 1) - 1)) by A41

          .= (f . ( len f));

          1 <= ( len g) by A36, A41, FINSEQ_1:def 3;

          hence thesis by A2, A34, A38, A51, A50, A43;

        end;

        Y is_reflexive_in X

        proof

          let x such that

           A52: x in X;

          set g = <*x*>;

          

           A53: for i st 1 <= i & i < ( len g) holds [(g . i), (g . (i + 1))] in (EqR1 \/ EqR2) by FINSEQ_1: 40;

          ( len g) = 1 & (g . 1) = x by FINSEQ_1: 40;

          hence thesis by A2, A52, A53;

        end;

        then ( field Y) = X & ( dom Y) = X by ORDERS_1: 13;

        then

        reconsider R1 = Y as Equivalence_Relation of X by A33, A3, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16;

        for x,y be object holds [x, y] in (EqR1 \/ EqR2) implies [x, y] in R1

        proof

          let x,y be object;

          assume

           A54: [x, y] in (EqR1 \/ EqR2);

          set g = <*x, y*>;

          

           A55: ( len g) = (1 + 1) by FINSEQ_1: 44;

          

           A56: (g . 1) = x by FINSEQ_1: 44;

          

           A57: for i st 1 <= i & i < ( len g) holds [(g . i), (g . (i + 1))] in (EqR1 \/ EqR2)

          proof

            let i;

            assume that

             A58: 1 <= i and

             A59: i < ( len g);

            i <= 1 by A55, A59, NAT_1: 13;

            then 1 = i by A58, XXREAL_0: 1;

            hence thesis by A54, A56, FINSEQ_1: 44;

          end;

          ( len g) = 2 by FINSEQ_1: 44;

          then

           A60: (g . 1) = x & (g . ( len g)) = y by FINSEQ_1: 44;

          x in X & y in X by A54, Lm1;

          hence thesis by A2, A55, A60, A57;

        end;

        then (EqR1 \/ EqR2) c= R1;

        then

         A61: (EqR1 "\/" EqR2) c= R1 by Def2;

        assume [x, y] in (EqR1 "\/" EqR2);

        then

        consider f be FinSequence such that

         A62: 1 <= ( len f) & x = (f . 1) & (y = (f . ( len f)) & for i st 1 <= i & i < ( len f) holds [(f . i), (f . (i + 1))] in (EqR1 \/ EqR2)) by A2, A61;

        take f;

        thus thesis by A62;

      end;

      given f be FinSequence such that

       A63: 1 <= ( len f) and

       A64: x = (f . 1) and

       A65: y = (f . ( len f)) and

       A66: for i st 1 <= i & i < ( len f) holds [(f . i), (f . (i + 1))] in (EqR1 \/ EqR2);

      defpred P[ Nat] means 1 <= $1 & $1 <= ( len f) implies [(f . 1), (f . $1)] in (EqR1 "\/" EqR2);

       A67:

      now

        let i;

        assume

         A68: P[i];

        thus P[(i + 1)]

        proof

          assume that

           A69: 1 <= (i + 1) and

           A70: (i + 1) <= ( len f);

          

           A71: 1 <= i or 1 = (i + 1) by A69, NAT_1: 8;

          

           A72: (EqR1 \/ EqR2) c= (EqR1 "\/" EqR2) by Def2;

          

           A73: i < ( len f) by A70, NAT_1: 13;

          now

            per cases by A71;

              suppose

               A74: 1 <= i;

              then [(f . i), (f . (i + 1))] in (EqR1 \/ EqR2) by A66, A73;

              hence thesis by A68, A70, A72, A74, Th7, NAT_1: 13;

            end;

              suppose

               A75: 0 = i;

               [(f . 1), (f . 1)] in EqR1 by A1, A64, Th5;

              then [(f . 1), (f . 1)] in (EqR1 \/ EqR2) by XBOOLE_0:def 3;

              hence thesis by A72, A75;

            end;

          end;

          hence thesis;

        end;

      end;

      

       A76: P[ 0 ];

      for i holds P[i] from NAT_1:sch 2( A76, A67);

      hence thesis by A63, A64, A65;

    end;

    theorem :: EQREL_1:29

    

     Th29: for E be Equivalence_Relation of X st E = (EqR1 \/ EqR2) holds for x st x in X holds ( Class (E,x)) = ( Class (EqR1,x)) or ( Class (E,x)) = ( Class (EqR2,x))

    proof

      let E be Equivalence_Relation of X such that

       A1: E = (EqR1 \/ EqR2);

      for x st x in X holds ( Class (E,x)) = ( Class (EqR1,x)) or ( Class (E,x)) = ( Class (EqR2,x))

      proof

        let x such that x in X;

        assume that

         A2: not ( Class (E,x)) = ( Class (EqR1,x)) and

         A3: not ( Class (E,x)) = ( Class (EqR2,x));

        consider y be object such that

         A4: y in ( Class (E,x)) & not y in ( Class (EqR1,x)) or y in ( Class (EqR1,x)) & not y in ( Class (E,x)) by A2, TARSKI: 2;

         A5:

        now

          assume that

           A6: y in ( Class (EqR1,x)) and

           A7: not y in ( Class (E,x));

           [y, x] in EqR1 by A6, Th19;

          then [y, x] in E by A1, XBOOLE_0:def 3;

          hence contradiction by A7, Th19;

        end;

        then

         A8: [y, x] in E by A4, Th19;

        consider z be object such that

         A9: z in ( Class (E,x)) & not z in ( Class (EqR2,x)) or z in ( Class (EqR2,x)) & not z in ( Class (E,x)) by A3, TARSKI: 2;

         A10:

        now

          assume that

           A11: z in ( Class (EqR2,x)) and

           A12: not z in ( Class (E,x));

           [z, x] in EqR2 by A11, Th19;

          then [z, x] in E by A1, XBOOLE_0:def 3;

          hence contradiction by A12, Th19;

        end;

        then

         A13: [z, x] in E by A9, Th19;

         not [z, x] in EqR2 by A9, A10, Th19;

        then

         A14: [z, x] in EqR1 by A1, A13, XBOOLE_0:def 3;

         A15:

        now

          assume [y, z] in EqR1;

          then

           A16: [z, y] in EqR1 by Th6;

           [x, z] in EqR1 by A14, Th6;

          then [x, y] in EqR1 by A16, Th7;

          then [y, x] in EqR1 by Th6;

          hence contradiction by A4, A5, Th19;

        end;

         not [y, x] in EqR1 by A4, A5, Th19;

        then

         A17: [y, x] in EqR2 by A1, A8, XBOOLE_0:def 3;

         A18:

        now

          assume

           A19: [y, z] in EqR2;

           [x, y] in EqR2 by A17, Th6;

          then [x, z] in EqR2 by A19, Th7;

          then [z, x] in EqR2 by Th6;

          hence contradiction by A9, A10, Th19;

        end;

         [x, z] in E by A13, Th6;

        then [y, z] in E by A8, Th7;

        hence contradiction by A1, A18, A15, XBOOLE_0:def 3;

      end;

      hence thesis;

    end;

    theorem :: EQREL_1:30

    (EqR1 \/ EqR2) = ( nabla X) implies EqR1 = ( nabla X) or EqR2 = ( nabla X)

    proof

      assume

       A1: (EqR1 \/ EqR2) = ( nabla X);

      X <> {} implies EqR1 = ( nabla X) or EqR2 = ( nabla X)

      proof

        set y = the Element of X;

         A2:

        now

          let x;

          assume

           A3: x in X;

          then ( Class (( nabla X),x)) = ( Class (EqR1,x)) or ( Class (( nabla X),x)) = ( Class (EqR2,x)) by A1, Th29;

          hence ( Class (EqR1,x)) = X or ( Class (EqR2,x)) = X by A3, Th26;

        end;

        assume X <> {} ;

        then ( Class (EqR1,y)) = X or ( Class (EqR2,y)) = X by A2;

        hence thesis by Th27;

      end;

      hence thesis;

    end;

    definition

      let X, EqR;

      :: EQREL_1:def3

      func Class EqR -> Subset-Family of X means

      : Def3: A in it iff ex x st x in X & A = ( Class (EqR,x));

      existence

      proof

        defpred P[ set] means ex x st x in X & $1 = ( Class (EqR,x));

        consider F be Subset-Family of X such that

         A1: for A holds A in F iff P[A] from SUBSET_1:sch 3;

        take F;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let F1,F2 be Subset-Family of X;

        assume that

         A2: for A holds A in F1 iff ex x st x in X & A = ( Class (EqR,x)) and

         A3: for A holds A in F2 iff ex x st x in X & A = ( Class (EqR,x));

        now

          let A;

          A in F1 iff ex x st x in X & A = ( Class (EqR,x)) by A2;

          hence A in F1 iff A in F2 by A3;

        end;

        hence thesis by SETFAM_1: 31;

      end;

    end

    theorem :: EQREL_1:31

    

     Th31: X = {} implies ( Class EqR) = {}

    proof

      assume that

       A1: X = {} and

       A2: ( Class EqR) <> {} ;

      set z = the Element of ( Class EqR);

      z is Subset of X by A2, TARSKI:def 3;

      then ex x st x in X & z = ( Class (EqR,x)) by A2, Def3;

      hence contradiction by A1;

    end;

    definition

      let X;

      :: EQREL_1:def4

      mode a_partition of X -> Subset-Family of X means

      : Def4: ( union it ) = X & for A st A in it holds A <> {} & for B st B in it holds A = B or A misses B;

      existence

      proof

        defpred P[ set] means ex x st x in X & $1 = {x};

        consider F be Subset-Family of X such that

         A1: for A be Subset of X holds A in F iff P[A] from SUBSET_1:sch 3;

        

         A2: for A st A in F holds A <> {} & for B st B in F holds A = B or A misses B

        proof

          let A;

          assume A in F;

          then

          consider x such that x in X and

           A3: A = {x} by A1;

          thus A <> {} by A3;

          let B;

          assume B in F;

          then

          consider y such that y in X and

           A4: B = {y} by A1;

          now

            assume

             A5: not x = y;

            for z be object st z in A holds not z in B

            proof

              let z be object;

              assume z in A;

              then not z = y by A3, A5, TARSKI:def 1;

              hence thesis by A4, TARSKI:def 1;

            end;

            hence A misses B by XBOOLE_0: 3;

          end;

          hence thesis by A3, A4;

        end;

        take F;

        now

          let y be object;

          now

            set Z = {y};

            assume

             A6: y in X;

            then Z is Subset of X by ZFMISC_1: 31;

            then y in Z & Z in F by A1, A6, TARSKI:def 1;

            hence ex Z st y in Z & Z in F;

          end;

          hence y in X iff ex Z st y in Z & Z in F;

        end;

        hence thesis by A2, TARSKI:def 4;

      end;

    end

    theorem :: EQREL_1:32

    

     Th32: for P be a_partition of {} holds P = {}

    proof

      let P be a_partition of {} ;

      assume not thesis;

      then

      consider Z be object such that

       A1: Z in P by XBOOLE_0:def 1;

      Z <> {} by A1, Def4;

      hence thesis by A1;

    end;

    registration

      let X be empty set;

      cluster -> empty for a_partition of X;

      coherence by Th32;

    end

    registration

      let X be empty set;

      cluster empty for a_partition of X;

      existence

      proof

        take the a_partition of X;

        thus thesis;

      end;

    end

    theorem :: EQREL_1:33

    

     Th33: ( Class EqR) is a_partition of X

    proof

      now

        let x be object;

        now

          consider Z such that

           A1: Z = ( Class (EqR,x));

          assume

           A2: x in X;

          then Z in ( Class EqR) by A1, Def3;

          hence ex Z st x in Z & Z in ( Class EqR) by A2, A1, Th20;

        end;

        hence x in X iff ex Z st x in Z & Z in ( Class EqR);

      end;

      hence ( union ( Class EqR)) = X by TARSKI:def 4;

      let A;

      assume A in ( Class EqR);

      then

       A3: ex x st x in X & A = ( Class (EqR,x)) by Def3;

      hence A <> {} by Th20;

      let B;

      assume B in ( Class EqR);

      then ex y st y in X & B = ( Class (EqR,y)) by Def3;

      hence thesis by A3, Th24;

    end;

    theorem :: EQREL_1:34

    

     Th34: for P be a_partition of X holds ex EqR st P = ( Class EqR)

    proof

      let P be a_partition of X;

      

       A1: X <> {} implies ex EqR st P = ( Class EqR)

      proof

        defpred P[ object, object] means ex A st A in P & $1 in A & $2 in A;

        assume X <> {} ;

        

         A2: for x, y, z st P[x, y] & P[y, z] holds P[x, z]

        proof

          let x, y, z;

          given A such that

           A3: A in P and

           A4: x in A & y in A;

          given B such that

           A5: B in P and

           A6: y in B & z in B;

          A = B or A misses B by A3, A5, Def4;

          hence thesis by A3, A4, A6, XBOOLE_0: 3;

        end;

        

         A7: ( union P) = X by Def4;

        

         A8: for x st x in X holds P[x, x]

        proof

          let x;

          assume x in X;

          then

          consider Z such that

           A9: x in Z and

           A10: Z in P by A7, TARSKI:def 4;

          reconsider A = Z as Subset of X by A10;

          take A;

          thus thesis by A9, A10;

        end;

        

         A11: for x, y st P[x, y] holds P[y, x];

        consider R be Equivalence_Relation of X such that

         A12: for x, y holds [x, y] in R iff x in X & y in X & P[x, y] from ExEqRel( A8, A11, A2);

        take R;

        now

          let A;

           A13:

          now

            set x = the Element of A;

            assume

             A14: A in P;

            then

             A15: A <> {} by Def4;

            then

             A16: x in X by TARSKI:def 3;

            now

              let y be object;

               A17:

              now

                assume y in ( Class (R,x));

                then [y, x] in R by Th19;

                then

                consider B such that

                 A18: B in P & y in B and

                 A19: x in B by A12;

                A meets B by A15, A19, XBOOLE_0: 3;

                hence y in A by A14, A18, Def4;

              end;

              now

                assume y in A;

                then [y, x] in R by A12, A14, A16;

                hence y in ( Class (R,x)) by Th19;

              end;

              hence y in A iff y in ( Class (R,x)) by A17;

            end;

            then A = ( Class (R,x)) by TARSKI: 2;

            hence A in ( Class R) by A16, Def3;

          end;

          now

            assume A in ( Class R);

            then

            consider x such that

             A20: x in X and

             A21: A = ( Class (R,x)) by Def3;

            x in ( Class (R,x)) by A20, Th20;

            then [x, x] in R by Th19;

            then

            consider B such that

             A22: B in P and

             A23: x in B and x in B by A12;

            now

              let y be object;

               A24:

              now

                assume y in A;

                then [y, x] in R by A21, Th19;

                then

                consider C such that

                 A25: C in P & y in C and

                 A26: x in C by A12;

                B meets C by A23, A26, XBOOLE_0: 3;

                hence y in B by A22, A25, Def4;

              end;

              now

                assume y in B;

                then [y, x] in R by A12, A22, A23;

                hence y in A by A21, Th19;

              end;

              hence y in A iff y in B by A24;

            end;

            hence A in P by A22, TARSKI: 2;

          end;

          hence A in P iff A in ( Class R) by A13;

        end;

        hence thesis by SETFAM_1: 31;

      end;

      X = {} implies ex EqR st P = ( Class EqR)

      proof

        set EqR1 = the Equivalence_Relation of X;

        assume

         A27: X = {} ;

        take EqR1;

        P = {} by A27;

        hence thesis by A27, Th31;

      end;

      hence thesis by A1;

    end;

    theorem :: EQREL_1:35

    for x st x in X holds [x, y] in EqR iff ( Class (EqR,x)) = ( Class (EqR,y)) by Lm2;

    theorem :: EQREL_1:36

    x in ( Class EqR) implies ex y be Element of X st x = ( Class (EqR,y))

    proof

      assume

       A1: x in ( Class EqR);

      then

      reconsider x as Subset of X;

      consider y such that

       A2: y in X and

       A3: x = ( Class (EqR,y)) by A1, Def3;

      reconsider y as Element of X by A2;

      take y;

      thus thesis by A3;

    end;

    begin

    registration

      let X be non empty set;

      cluster -> non empty for a_partition of X;

      coherence

      proof

        set x = the Element of X;

        let P be a_partition of X;

        ( union P) = X by Def4;

        then ex A be set st x in A & A in P by TARSKI:def 4;

        hence thesis;

      end;

    end

    registration

      let X be set;

      cluster -> with_non-empty_elements for a_partition of X;

      coherence

      proof

        let P be a_partition of X;

        assume {} in P;

        hence contradiction by Def4;

      end;

    end

    definition

      let X be set, R be Equivalence_Relation of X;

      :: original: Class

      redefine

      func Class R -> a_partition of X ;

      coherence by Th33;

    end

    registration

      let I be non empty set, R be Equivalence_Relation of I;

      cluster ( Class R) -> non empty;

      coherence ;

    end

    registration

      let I be non empty set, R be Equivalence_Relation of I;

      cluster ( Class R) -> with_non-empty_elements;

      coherence ;

    end

    notation

      let I be non empty set, R be Equivalence_Relation of I;

      let x be Element of I;

      synonym EqClass (R,x) for Class (R,x);

    end

    definition

      let I be non empty set, R be Equivalence_Relation of I;

      let x be Element of I;

      :: original: EqClass

      redefine

      func EqClass (R,x) -> Element of ( Class R) ;

      coherence

      proof

        thus ( Class (R,x)) is Element of ( Class R) by Def3;

      end;

    end

    definition

      let X be set;

      :: EQREL_1:def5

      func SmallestPartition X -> set equals ( Class ( id X));

      coherence ;

    end

    definition

      let X be set;

      :: original: SmallestPartition

      redefine

      func SmallestPartition X -> a_partition of X ;

      correctness ;

    end

    theorem :: EQREL_1:37

    for X be non empty set holds ( SmallestPartition X) = the set of all {x} where x be Element of X

    proof

      let X be non empty set;

      set Y = the set of all {x} where x be Element of X;

      hereby

        let x be object;

        assume x in ( SmallestPartition X);

        then

        consider y be object such that

         A1: y in X and

         A2: x = ( Class (( id X),y)) by Def3;

        x = {y} by A1, A2, Th25;

        hence x in Y by A1;

      end;

      let x be object;

      assume x in Y;

      then

      consider y be Element of X such that

       A3: x = {y};

      ( Class (( id X),y)) = x by A3, Th25;

      hence thesis by Def3;

    end;

    reserve X for non empty set,

x for Element of X;

    definition

      let X be non empty set, x be Element of X, S1 be a_partition of X;

      :: EQREL_1:def6

      func EqClass (x,S1) -> Subset of X means

      : Def6: x in it & it in S1;

      existence

      proof

        consider EQR be Equivalence_Relation of X such that

         A1: S1 = ( Class EQR) by Th34;

        take ( Class (EQR,x));

        thus x in ( Class (EQR,x)) by Th20;

        thus thesis by A1, Def3;

      end;

      uniqueness by Def4, XBOOLE_0: 3;

    end

    theorem :: EQREL_1:38

    

     Th38: for S1,S2 be a_partition of X st (for x be Element of X holds ( EqClass (x,S1)) = ( EqClass (x,S2))) holds S1 = S2

    proof

      let S1,S2 be a_partition of X;

      assume

       A1: for x be Element of X holds ( EqClass (x,S1)) = ( EqClass (x,S2));

      now

        let P be Subset of X;

        thus P in S1 implies P in S2

        proof

          set x = the Element of P;

          assume

           A2: P in S1;

          then

           A3: P is non empty by Def4;

          then x in P;

          then

          reconsider x as Element of X;

          P = ( EqClass (x,S1)) by A2, A3, Def6;

          then P = ( EqClass (x,S2)) by A1;

          hence thesis by Def6;

        end;

        thus P in S2 implies P in S1

        proof

          set x = the Element of P;

          assume

           A4: P in S2;

          then

           A5: P <> {} by Def4;

          then x in P;

          then

          reconsider x as Element of X;

          P = ( EqClass (x,S2)) by A4, A5, Def6;

          then P = ( EqClass (x,S1)) by A1;

          hence thesis by Def6;

        end;

      end;

      hence thesis by SETFAM_1: 31;

    end;

    theorem :: EQREL_1:39

    

     Th39: for X be non empty set holds {X} is a_partition of X

    proof

      let X be non empty set;

      reconsider A1 = {X} as Subset-Family of X by ZFMISC_1: 68;

      

       A1: for A be Subset of X st A in A1 holds A <> {} & for B be Subset of X st B in A1 holds A = B or A misses B

      proof

        let A be Subset of X;

        assume

         A2: A in A1;

        hence A <> {} by TARSKI:def 1;

        let B be Subset of X;

        assume B in A1;

        then B = X by TARSKI:def 1;

        hence thesis by A2, TARSKI:def 1;

      end;

      ( union A1) = X;

      hence thesis by A1, Def4;

    end;

    definition

      let X be set;

      mode Family-Class of X is Subset-Family of ( bool X);

    end

    definition

      let X be set;

      let F be Family-Class of X;

      :: EQREL_1:def7

      attr F is partition-membered means

      : Def7: for S be set st S in F holds S is a_partition of X;

    end

    registration

      let X be set;

      cluster partition-membered for Family-Class of X;

      existence

      proof

        reconsider E = {} as Family-Class of X by XBOOLE_1: 2;

        take E;

        let S be set;

        assume S in E;

        hence thesis;

      end;

    end

    definition

      let X be set;

      mode Part-Family of X is partition-membered Family-Class of X;

    end

    reserve F for Part-Family of X;

    registration

      let X be non empty set;

      cluster non empty for a_partition of X;

      existence

      proof

        take {X};

        thus thesis by Th39;

      end;

    end

    theorem :: EQREL_1:40

    

     Th40: for X be set, p be a_partition of X holds {p} is Part-Family of X

    proof

      let X be set;

      let p be a_partition of X;

      for x be set st x in {p} holds x is a_partition of X by TARSKI:def 1;

      hence thesis by Def7;

    end;

    registration

      let X be set;

      cluster non empty for Part-Family of X;

      existence

      proof

        set p = the a_partition of X;

        reconsider P = {p} as Part-Family of X by Th40;

        take P;

        thus thesis;

      end;

    end

    theorem :: EQREL_1:41

    

     Th41: for S1 be a_partition of X, x,y be Element of X holds ( EqClass (x,S1)) meets ( EqClass (y,S1)) implies ( EqClass (x,S1)) = ( EqClass (y,S1))

    proof

      let S1 be a_partition of X;

      let x,y be Element of X;

      consider EQR be Equivalence_Relation of X such that

       A1: S1 = ( Class EQR) by Th34;

      

       A2: y in ( Class (EQR,y)) by Th20;

      ( Class (EQR,y)) in S1 by A1, Def3;

      then

       A3: ( Class (EQR,y)) = ( EqClass (y,S1)) by A2, Def6;

      

       A4: x in ( Class (EQR,x)) by Th20;

      ( Class (EQR,x)) in S1 by A1, Def3;

      then

       A5: ( Class (EQR,x)) = ( EqClass (x,S1)) by A4, Def6;

      assume ( EqClass (x,S1)) meets ( EqClass (y,S1));

      hence thesis by A5, A3, Th24;

    end;

    

     Lm3: for A be set holds A in { ( EqClass (x,S)) where S be a_partition of X : S in F } implies ex T be a_partition of X st T in F & A = ( EqClass (x,T))

    proof

      let A be set;

      assume A in { ( EqClass (x,S)) where S be a_partition of X : S in F };

      then

      consider S be a_partition of X such that

       A1: A = ( EqClass (x,S)) & S in F;

      take S;

      thus thesis by A1;

    end;

    theorem :: EQREL_1:42

    for A be set, X be non empty set, S be a_partition of X holds A in S implies ex x be Element of X st A = ( EqClass (x,S))

    proof

      let A be set, X be non empty set, S be a_partition of X;

      assume

       A1: A in S;

      then A is non empty by Def4;

      then

      consider x be object such that

       A2: x in A;

      take x;

      thus thesis by A1, A2, Def6;

    end;

    definition

      let X be non empty set, F be non empty Part-Family of X;

      :: EQREL_1:def8

      func Intersection F -> non empty a_partition of X means for x be Element of X holds ( EqClass (x,it )) = ( meet { ( EqClass (x,S)) where S be a_partition of X : S in F });

      uniqueness

      proof

        given S1,S2 be a_partition of X such that

         A1: for x be Element of X holds ( EqClass (x,S1)) = ( meet { ( EqClass (x,S)) where S be a_partition of X : S in F }) and

         A2: for x be Element of X holds ( EqClass (x,S2)) = ( meet { ( EqClass (x,S)) where S be a_partition of X : S in F }) and

         A3: not S1 = S2;

        now

          let x be Element of X;

          ( EqClass (x,S1)) = ( meet { ( EqClass (x,S)) where S be a_partition of X : S in F }) by A1;

          hence ( EqClass (x,S1)) = ( EqClass (x,S2)) by A2;

        end;

        hence contradiction by A3, Th38;

      end;

      existence

      proof

        thus ex G be non empty a_partition of X st for x be Element of X holds ( EqClass (x,G)) = ( meet { ( EqClass (x,S)) where S be a_partition of X : S in F })

        proof

          set G = the set of all ( meet { ( EqClass (x,S)) where S be a_partition of X : S in F }) where x be Element of X;

          G c= ( bool X)

          proof

            let y be object;

            reconsider yy = y as set by TARSKI: 1;

            assume y in G;

            then

            consider x be Element of X such that

             A4: y = ( meet { ( EqClass (x,S)) where S be a_partition of X : S in F });

            yy c= X

            proof

              let e be object;

              consider T be object such that

               A5: T in F by XBOOLE_0:def 1;

              reconsider T as a_partition of X by A5, Def7;

              ( EqClass (x,T)) in { ( EqClass (x,S)) where S be a_partition of X : S in F } by A5;

              then

              consider f be set such that

               A6: f in { ( EqClass (x,S)) where S be a_partition of X : S in F };

              consider S be a_partition of X such that

               A7: f = ( EqClass (x,S)) and S in F by A6;

              assume e in yy;

              then e in ( EqClass (x,S)) by A4, A6, A7, SETFAM_1:def 1;

              hence thesis;

            end;

            hence thesis;

          end;

          then

          reconsider G as Subset-Family of X;

          G is a_partition of X

          proof

            X c= ( union G)

            proof

              let a be object;

              consider T be object such that

               A8: T in F by XBOOLE_0:def 1;

              assume a in X;

              then

              reconsider a1 = a as Element of X;

              reconsider T as a_partition of X by A8, Def7;

              

               A9: ( meet { ( EqClass (a1,S)) where S be a_partition of X : S in F }) in G;

              

               A10: for T be set st T in { ( EqClass (a1,S)) where S be a_partition of X : S in F } holds a1 in T

              proof

                let T be set;

                assume T in { ( EqClass (a1,S)) where S be a_partition of X : S in F };

                then ex A be a_partition of X st T = ( EqClass (a1,A)) & A in F;

                hence thesis by Def6;

              end;

              ( EqClass (a1,T)) in { ( EqClass (a1,S)) where S be a_partition of X : S in F } by A8;

              then a in ( meet { ( EqClass (a1,S)) where S be a_partition of X : S in F }) by A10, SETFAM_1:def 1;

              hence thesis by A9, TARSKI:def 4;

            end;

            hence ( union G) = X;

            let A be Subset of X;

            consider T be object such that

             A11: T in F by XBOOLE_0:def 1;

            reconsider T as a_partition of X by A11, Def7;

            assume

             A12: A in G;

            then

            consider x be Element of X such that

             A13: A = ( meet { ( EqClass (x,S)) where S be a_partition of X : S in F });

            

             A14: for Y be set st Y in { ( EqClass (x,S)) where S be a_partition of X : S in F } holds x in Y

            proof

              let Y be set;

              assume Y in { ( EqClass (x,S)) where S be a_partition of X : S in F };

              then ex T be a_partition of X st Y = ( EqClass (x,T)) & T in F;

              hence thesis by Def6;

            end;

            ( EqClass (x,T)) in { ( EqClass (x,S)) where S be a_partition of X : S in F } by A11;

            hence A <> {} by A13, A14, SETFAM_1:def 1;

            consider x be Element of X such that

             A15: A = ( meet { ( EqClass (x,S)) where S be a_partition of X : S in F }) by A12;

            let B be Subset of X;

            assume B in G;

            then

            consider y be Element of X such that

             A16: B = ( meet { ( EqClass (y,S)) where S be a_partition of X : S in F });

            thus A = B or A misses B

            proof

              

               A17: { ( EqClass (y,S)) where S be a_partition of X : S in F } is non empty

              proof

                consider T be object such that

                 A18: T in F by XBOOLE_0:def 1;

                reconsider T as a_partition of X by A18, Def7;

                ( EqClass (y,T)) in { ( EqClass (y,S)) where S be a_partition of X : S in F } by A18;

                hence thesis;

              end;

              

               A19: { ( EqClass (x,S)) where S be a_partition of X : S in F } is non empty

              proof

                consider T be object such that

                 A20: T in F by XBOOLE_0:def 1;

                reconsider T as a_partition of X by A20, Def7;

                ( EqClass (x,T)) in { ( EqClass (x,S)) where S be a_partition of X : S in F } by A20;

                hence thesis;

              end;

              now

                assume A meets B;

                then

                consider c be object such that

                 A21: c in A & c in B by XBOOLE_0: 3;

                c in (( meet { ( EqClass (x,S)) where S be a_partition of X : S in F }) /\ ( meet { ( EqClass (y,S)) where S be a_partition of X : S in F })) by A15, A16, A21, XBOOLE_0:def 4;

                then

                 A22: c in ( meet ({ ( EqClass (x,S)) where S be a_partition of X : S in F } \/ { ( EqClass (y,S)) where S be a_partition of X : S in F })) by A19, A17, SETFAM_1: 9;

                 A23:

                now

                  let T be a_partition of X;

                  assume T in F;

                  then ( EqClass (y,T)) in { ( EqClass (y,S)) where S be a_partition of X : S in F };

                  then ( EqClass (y,T)) in ({ ( EqClass (x,S)) where S be a_partition of X : S in F } \/ { ( EqClass (y,S)) where S be a_partition of X : S in F }) by XBOOLE_0:def 3;

                  hence c in ( EqClass (y,T)) by A22, SETFAM_1:def 1;

                end;

                 A24:

                now

                  let T be a_partition of X;

                  assume T in F;

                  then ( EqClass (x,T)) in { ( EqClass (x,S)) where S be a_partition of X : S in F };

                  then ( EqClass (x,T)) in ({ ( EqClass (x,S)) where S be a_partition of X : S in F } \/ { ( EqClass (y,S)) where S be a_partition of X : S in F }) by XBOOLE_0:def 3;

                  hence c in ( EqClass (x,T)) by A22, SETFAM_1:def 1;

                end;

                

                 A25: for T be a_partition of X st T in F holds ex A be object st A in ( EqClass (x,T)) & A in ( EqClass (y,T))

                proof

                  let T be a_partition of X;

                  assume

                   A26: T in F;

                  take c;

                  thus thesis by A24, A23, A26;

                end;

                

                 A27: for T be a_partition of X st T in F holds ( EqClass (x,T)) meets ( EqClass (y,T))

                proof

                  let T be a_partition of X;

                  assume T in F;

                  then ex A be object st A in ( EqClass (x,T)) & A in ( EqClass (y,T)) by A25;

                  hence thesis by XBOOLE_0: 3;

                end;

                

                 A28: { ( EqClass (y,S)) where S be a_partition of X : S in F } c= { ( EqClass (x,S)) where S be a_partition of X : S in F }

                proof

                  let A be object;

                  assume A in { ( EqClass (y,S)) where S be a_partition of X : S in F };

                  then

                  consider T be a_partition of X such that

                   A29: T in F and

                   A30: A = ( EqClass (y,T)) by Lm3;

                  A = ( EqClass (x,T)) by A27, A29, A30, Th41;

                  hence thesis by A29;

                end;

                { ( EqClass (x,S)) where S be a_partition of X : S in F } c= { ( EqClass (y,S)) where S be a_partition of X : S in F }

                proof

                  let A be object;

                  assume A in { ( EqClass (x,S)) where S be a_partition of X : S in F };

                  then

                  consider T be a_partition of X such that

                   A31: T in F and

                   A32: A = ( EqClass (x,T)) by Lm3;

                  A = ( EqClass (y,T)) by A27, A31, A32, Th41;

                  hence thesis by A31;

                end;

                hence thesis by A15, A16, A28, XBOOLE_0:def 10;

              end;

              hence thesis;

            end;

          end;

          then

          reconsider G as non empty a_partition of X;

          take G;

          for x be Element of X holds ( EqClass (x,G)) = ( meet { ( EqClass (x,S)) where S be a_partition of X : S in F })

          proof

            let x be Element of X;

             A33:

            now

              let Y be set;

              assume Y in { ( EqClass (x,S)) where S be a_partition of X : S in F };

              then ex T be a_partition of X st Y = ( EqClass (x,T)) & T in F;

              hence x in Y by Def6;

            end;

            { ( EqClass (x,S)) where S be a_partition of X : S in F } is non empty

            proof

              consider T be object such that

               A34: T in F by XBOOLE_0:def 1;

              reconsider T as a_partition of X by A34, Def7;

              ( EqClass (x,T)) in { ( EqClass (x,S)) where S be a_partition of X : S in F } by A34;

              hence thesis;

            end;

            then ( meet { ( EqClass (x,S)) where S be a_partition of X : S in F }) in G & x in ( meet { ( EqClass (x,S)) where S be a_partition of X : S in F }) by A33, SETFAM_1:def 1;

            hence thesis by Def6;

          end;

          hence thesis;

        end;

      end;

    end

    theorem :: EQREL_1:43

    

     Th43: for X be non empty set, S be a_partition of X, A be Subset of S holds (( union S) \ ( union A)) = ( union (S \ A))

    proof

      let X be non empty set;

      let S be a_partition of X;

      let A be Subset of S;

      thus (( union S) \ ( union A)) c= ( union (S \ A))

      proof

        let y be object;

        assume

         A1: y in (( union S) \ ( union A));

        then y in ( union S) by XBOOLE_0:def 5;

        then

        consider z be set such that

         A2: y in z and

         A3: z in S by TARSKI:def 4;

         not y in ( union A) by A1, XBOOLE_0:def 5;

        then not z in A by A2, TARSKI:def 4;

        then z in (S \ A) by A3, XBOOLE_0:def 5;

        hence thesis by A2, TARSKI:def 4;

      end;

      thus ( union (S \ A)) c= (( union S) \ ( union A))

      proof

        let y be object;

        assume y in ( union (S \ A));

        then

        consider z be set such that

         A4: y in z and

         A5: z in (S \ A) by TARSKI:def 4;

        

         A6: z in S by A5, XBOOLE_0:def 5;

        

         A7: not z in A by A5, XBOOLE_0:def 5;

         A8:

        now

          let w be set;

          assume

           A9: w in A;

          then w in S;

          then z misses w by A6, A7, A9, Def4;

          hence not y in w by A4, XBOOLE_0: 3;

        end;

         A10:

        now

          assume y in ( union A);

          then ex v be set st y in v & v in A by TARSKI:def 4;

          hence contradiction by A8;

        end;

        y in ( union S) by A4, A6, TARSKI:def 4;

        hence thesis by A10, XBOOLE_0:def 5;

      end;

    end;

    theorem :: EQREL_1:44

    for X be non empty set, A be Subset of X, S be a_partition of X holds A in S implies ( union (S \ {A})) = (X \ A)

    proof

      let X be non empty set;

      let A be Subset of X;

      let S be a_partition of X;

      assume

       A1: A in S;

       {A} c= S by A1, TARSKI:def 1;

      then

      reconsider AA = {A} as Subset of S;

      

      thus ( union (S \ {A})) = (( union S) \ ( union AA)) by Th43

      .= (X \ ( union {A})) by Def4

      .= (X \ A);

    end;

    registration

      let A be empty set;

      cluster -> empty for a_partition of A;

      coherence ;

    end

    theorem :: EQREL_1:45

     {} is a_partition of {}

    proof

      reconsider A = {} as Subset-Family of {} by XBOOLE_1: 2;

      ( union A) = {} & for a be Subset of {} st a in A holds a <> {} & for b be Subset of {} st b in A holds a = b or a misses b;

      hence thesis by Def4;

    end;

    registration

      let A be empty set;

      cluster empty for a_partition of A;

      existence

      proof

        take the a_partition of A;

        thus thesis;

      end;

    end

    begin

    reserve e,u,v for object,

E,X,Y,X1 for set;

    theorem :: EQREL_1:46

    for F be Function st X c= (F " X1) holds (F .: X) c= X1

    proof

      let F be Function;

      assume X c= (F " X1);

      then

       A1: (F .: X) c= (F .: (F " X1)) by RELAT_1: 123;

      (F .: (F " X1)) c= X1 by FUNCT_1: 75;

      hence thesis by A1;

    end;

    theorem :: EQREL_1:47

    

     Th47: E c= [:X, Y:] implies (( .: ( pr1 (X,Y))) . E) = (( pr1 (X,Y)) .: E)

    proof

      assume E c= [:X, Y:];

      then E c= ( dom ( pr1 (X,Y))) by FUNCT_3:def 4;

      hence thesis by FUNCT_3:def 1;

    end;

    theorem :: EQREL_1:48

    

     Th48: E c= [:X, Y:] implies (( .: ( pr2 (X,Y))) . E) = (( pr2 (X,Y)) .: E)

    proof

      assume E c= [:X, Y:];

      then E c= ( dom ( pr2 (X,Y))) by FUNCT_3:def 5;

      hence thesis by FUNCT_3:def 1;

    end;

    theorem :: EQREL_1:49

    

     Th49: for X1 be Subset of X, Y1 be Subset of Y st [:X1, Y1:] <> {} holds (( pr1 (X,Y)) .: [:X1, Y1:]) = X1 & (( pr2 (X,Y)) .: [:X1, Y1:]) = Y1

    proof

      let X1 be Subset of X, Y1 be Subset of Y;

      assume

       A1: [:X1, Y1:] <> {} ;

      then

       A2: X1 <> {} ;

      

       A3: Y1 <> {} by A1;

      

       A4: X <> {} by A2;

      now

        set y = the Element of Y1;

        let x be object;

        thus x in (( pr1 (X,Y)) .: [:X1, Y1:]) implies x in X1

        proof

          assume x in (( pr1 (X,Y)) .: [:X1, Y1:]);

          then

          consider u such that

           A5: u in [:X, Y:] and

           A6: u in [:X1, Y1:] & x = (( pr1 (X,Y)) . u) by FUNCT_2: 64;

          

           A7: (u `2 ) in Y by A5, MCART_1: 10;

          (u `1 ) in X1 & x = (( pr1 (X,Y)) . ((u `1 ),(u `2 ))) by A6, MCART_1: 10, MCART_1: 21;

          hence thesis by A7, FUNCT_3:def 4;

        end;

        assume

         A8: x in X1;

        y in Y by A3, TARSKI:def 3;

        then

         A9: x = (( pr1 (X,Y)) . (x,y)) by A8, FUNCT_3:def 4;

         [x, y] in [:X1, Y1:] by A3, A8, ZFMISC_1: 87;

        hence x in (( pr1 (X,Y)) .: [:X1, Y1:]) by A4, A9, FUNCT_2: 35;

      end;

      hence (( pr1 (X,Y)) .: [:X1, Y1:]) = X1 by TARSKI: 2;

      

       A10: Y <> {} by A3;

      now

        set x = the Element of X1;

        let y be object;

        thus y in (( pr2 (X,Y)) .: [:X1, Y1:]) implies y in Y1

        proof

          assume y in (( pr2 (X,Y)) .: [:X1, Y1:]);

          then

          consider u such that

           A11: u in [:X, Y:] and

           A12: u in [:X1, Y1:] & y = (( pr2 (X,Y)) . u) by FUNCT_2: 64;

          

           A13: (u `1 ) in X by A11, MCART_1: 10;

          (u `2 ) in Y1 & y = (( pr2 (X,Y)) . ((u `1 ),(u `2 ))) by A12, MCART_1: 10, MCART_1: 21;

          hence thesis by A13, FUNCT_3:def 5;

        end;

        assume

         A14: y in Y1;

        x in X by A2, TARSKI:def 3;

        then

         A15: y = (( pr2 (X,Y)) . (x,y)) by A14, FUNCT_3:def 5;

         [x, y] in [:X1, Y1:] by A2, A14, ZFMISC_1: 87;

        hence y in (( pr2 (X,Y)) .: [:X1, Y1:]) by A10, A15, FUNCT_2: 35;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: EQREL_1:50

    

     Th50: for X1 be Subset of X, Y1 be Subset of Y st [:X1, Y1:] <> {} holds (( .: ( pr1 (X,Y))) . [:X1, Y1:]) = X1 & (( .: ( pr2 (X,Y))) . [:X1, Y1:]) = Y1

    proof

      let X1 be Subset of X, Y1 be Subset of Y;

      assume

       A1: [:X1, Y1:] <> {} ;

      

      thus (( .: ( pr1 (X,Y))) . [:X1, Y1:]) = (( pr1 (X,Y)) .: [:X1, Y1:]) by Th47

      .= X1 by A1, Th49;

      

      thus (( .: ( pr2 (X,Y))) . [:X1, Y1:]) = (( pr2 (X,Y)) .: [:X1, Y1:]) by Th48

      .= Y1 by A1, Th49;

    end;

    theorem :: EQREL_1:51

    for A be Subset of [:X, Y:], H be Subset-Family of [:X, Y:] st for E st E in H holds E c= A & ex X1 be Subset of X, Y1 be Subset of Y st E = [:X1, Y1:] holds [:( union (( .: ( pr1 (X,Y))) .: H)), ( meet (( .: ( pr2 (X,Y))) .: H)):] c= A

    proof

      let A be Subset of [:X, Y:], H be Subset-Family of [:X, Y:] such that

       A1: for E st E in H holds E c= A & ex X1 be Subset of X, Y1 be Subset of Y st E = [:X1, Y1:];

      let u,v be object;

      assume

       A2: [u, v] in [:( union (( .: ( pr1 (X,Y))) .: H)), ( meet (( .: ( pr2 (X,Y))) .: H)):];

      then

       A3: v in ( meet (( .: ( pr2 (X,Y))) .: H)) by ZFMISC_1: 87;

      u in ( union (( .: ( pr1 (X,Y))) .: H)) by A2, ZFMISC_1: 87;

      then

      consider x be set such that

       A4: u in x and

       A5: x in (( .: ( pr1 (X,Y))) .: H) by TARSKI:def 4;

      consider y be object such that y in ( dom ( .: ( pr1 (X,Y)))) and

       A6: y in H and

       A7: x = (( .: ( pr1 (X,Y))) . y) by A5, FUNCT_1:def 6;

      reconsider y as set by TARSKI: 1;

      consider X1 be Subset of X, Y1 be Subset of Y such that

       A8: y = [:X1, Y1:] by A1, A6;

      

       A9: y <> {} by A4, A7, FUNCT_3: 8;

      y in ( bool [:X, Y:]) by A6;

      then y in ( bool ( dom ( pr2 (X,Y)))) by FUNCT_3:def 5;

      then y in ( dom ( .: ( pr2 (X,Y)))) by FUNCT_3:def 1;

      then (( .: ( pr2 (X,Y))) . y) in (( .: ( pr2 (X,Y))) .: H) by A6, FUNCT_1:def 6;

      then Y1 in (( .: ( pr2 (X,Y))) .: H) by A8, A9, Th50;

      then

       A10: v in Y1 by A3, SETFAM_1:def 1;

      u in X1 by A4, A7, A8, A9, Th50;

      then

       A11: [u, v] in y by A8, A10, ZFMISC_1: 87;

      y c= A by A1, A6;

      hence thesis by A11;

    end;

    theorem :: EQREL_1:52

    for A be Subset of [:X, Y:], H be Subset-Family of [:X, Y:] st for E st E in H holds E c= A & ex X1 be Subset of X, Y1 be Subset of Y st E = [:X1, Y1:] holds [:( meet (( .: ( pr1 (X,Y))) .: H)), ( union (( .: ( pr2 (X,Y))) .: H)):] c= A

    proof

      let A be Subset of [:X, Y:], H be Subset-Family of [:X, Y:] such that

       A1: for E st E in H holds E c= A & ex X1 be Subset of X, Y1 be Subset of Y st E = [:X1, Y1:];

      let u,v be object;

      assume

       A2: [u, v] in [:( meet (( .: ( pr1 (X,Y))) .: H)), ( union (( .: ( pr2 (X,Y))) .: H)):];

      then

       A3: u in ( meet (( .: ( pr1 (X,Y))) .: H)) by ZFMISC_1: 87;

      v in ( union (( .: ( pr2 (X,Y))) .: H)) by A2, ZFMISC_1: 87;

      then

      consider x be set such that

       A4: v in x and

       A5: x in (( .: ( pr2 (X,Y))) .: H) by TARSKI:def 4;

      consider y be object such that y in ( dom ( .: ( pr2 (X,Y)))) and

       A6: y in H and

       A7: x = (( .: ( pr2 (X,Y))) . y) by A5, FUNCT_1:def 6;

      reconsider y as set by TARSKI: 1;

      consider X1 be Subset of X, Y1 be Subset of Y such that

       A8: y = [:X1, Y1:] by A1, A6;

      

       A9: y <> {} by A4, A7, FUNCT_3: 8;

      y in ( bool [:X, Y:]) by A6;

      then y in ( bool ( dom ( pr1 (X,Y)))) by FUNCT_3:def 4;

      then y in ( dom ( .: ( pr1 (X,Y)))) by FUNCT_3:def 1;

      then (( .: ( pr1 (X,Y))) . y) in (( .: ( pr1 (X,Y))) .: H) by A6, FUNCT_1:def 6;

      then X1 in (( .: ( pr1 (X,Y))) .: H) by A8, A9, Th50;

      then

       A10: u in X1 by A3, SETFAM_1:def 1;

      v in Y1 by A4, A7, A8, A9, Th50;

      then

       A11: [u, v] in y by A8, A10, ZFMISC_1: 87;

      y c= A by A1, A6;

      hence thesis by A11;

    end;

    theorem :: EQREL_1:53

    for X be set, Y be non empty set, f be Function of X, Y holds for H be Subset-Family of X holds ( union (( .: f) .: H)) = (f .: ( union H))

    proof

      let X be set, Y be non empty set, f be Function of X, Y;

      let H be Subset-Family of X;

      ( dom f) = X by FUNCT_2:def 1;

      hence thesis by FUNCT_3: 14;

    end;

    reserve X,Y,Z for non empty set;

    theorem :: EQREL_1:54

    for X be set, a be Subset-Family of X holds ( union ( union a)) = ( union { ( union A) where A be Subset of X : A in a })

    proof

      let X be set, a be Subset-Family of X;

      thus ( union ( union a)) c= ( union { ( union A) where A be Subset of X : A in a })

      proof

        let e be object;

        assume e in ( union ( union a));

        then

        consider B be set such that

         A1: e in B and

         A2: B in ( union a) by TARSKI:def 4;

        consider C be set such that

         A3: B in C and

         A4: C in a by A2, TARSKI:def 4;

        

         A5: ( union C) in { ( union A) where A be Subset of X : A in a } by A4;

        e in ( union C) by A1, A3, TARSKI:def 4;

        hence thesis by A5, TARSKI:def 4;

      end;

      let e be object;

      assume e in ( union { ( union A) where A be Subset of X : A in a });

      then

      consider c be set such that

       A6: e in c and

       A7: c in { ( union A) where A be Subset of X : A in a } by TARSKI:def 4;

      consider A be Subset of X such that

       A8: c = ( union A) and

       A9: A in a by A7;

      consider b be set such that

       A10: e in b and

       A11: b in A by A6, A8, TARSKI:def 4;

      b in ( union a) by A9, A11, TARSKI:def 4;

      hence thesis by A10, TARSKI:def 4;

    end;

    theorem :: EQREL_1:55

    

     Th55: for X be set holds for D be Subset-Family of X st ( union D) = X holds for A be Subset of D, B be Subset of X st B = ( union A) holds (B ` ) c= ( union (A ` ))

    proof

      let X be set;

      let D be Subset-Family of X such that

       A1: ( union D) = X;

      let A be Subset of D, B be Subset of X such that

       A2: B = ( union A);

      let e be object;

      assume

       A3: e in (B ` );

      then

      consider u be set such that

       A4: e in u and

       A5: u in D by A1, TARSKI:def 4;

       not e in B by A3, XBOOLE_0:def 5;

      then not u in A by A2, A4, TARSKI:def 4;

      then u in (A ` ) by A5, SUBSET_1: 29;

      hence thesis by A4, TARSKI:def 4;

    end;

    theorem :: EQREL_1:56

    for F be Function of X, Y, G be Function of X, Z st for x,x9 be Element of X st (F . x) = (F . x9) holds (G . x) = (G . x9) holds ex H be Function of Y, Z st (H * F) = G

    proof

      let F be Function of X, Y, G be Function of X, Z;

      defpred P[ object, object] means not (ex x be Element of X st $1 = (F . x)) or for x be Element of X st $1 = (F . x) holds $2 = (G . x);

      assume

       A1: for x,x9 be Element of X st (F . x) = (F . x9) holds (G . x) = (G . x9);

       A2:

      now

        let e be object such that e in Y;

        now

          per cases ;

            case ex x be Element of X st e = (F . x);

            then

            consider x be Element of X such that

             A3: e = (F . x);

            take u = (G . x);

            thus u in Z & ((ex x be Element of X st e = (F . x)) implies ex x be Element of X st e = (F . x) & u = (G . x)) by A3;

          end;

            case

             A4: not ex x be Element of X st e = (F . x);

            set u = the Element of Z;

            u in Z;

            hence ex u st u in Z & ((ex x be Element of X st e = (F . x)) implies ex x be Element of X st e = (F . x) & u = (G . x)) by A4;

          end;

        end;

        then

        consider u such that

         A5: u in Z and

         A6: (ex x be Element of X st e = (F . x)) implies ex x be Element of X st e = (F . x) & u = (G . x);

        reconsider u as object;

        take u;

        thus u in Z by A5;

        thus P[e, u] by A1, A6;

      end;

      consider H be Function of Y, Z such that

       A7: for e be object st e in Y holds P[e, (H . e)] from FUNCT_2:sch 1( A2);

      take H;

      now

        let x be Element of X;

        

        thus ((H * F) . x) = (H . (F . x)) by FUNCT_2: 15

        .= (G . x) by A7;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: EQREL_1:57

    for X, Y, Z holds for y be Element of Y, F be Function of X, Y, G be Function of Y, Z holds (F " {y}) c= ((G * F) " {(G . y)})

    proof

      let X, Y, Z;

      let y be Element of Y, F be Function of X, Y, G be Function of Y, Z;

      (F " {y}) c= ((G * F) " ( Im (G,y))) by FUNCT_2: 44;

      hence thesis by SETWISEO: 8;

    end;

    theorem :: EQREL_1:58

    for F be Function of X, Y, x be Element of X, z be Element of Z holds ( [:F, ( id Z):] . (x,z)) = [(F . x), z]

    proof

      let F be Function of X, Y, x be Element of X, z be Element of Z;

      

      thus ( [:F, ( id Z):] . (x,z)) = [(F . x), (( id Z) . z)] by FUNCT_3: 75

      .= [(F . x), z];

    end;

    theorem :: EQREL_1:59

    for F be Function of X, Y, A be Subset of X, B be Subset of Z holds ( [:F, ( id Z):] .: [:A, B:]) = [:(F .: A), B:]

    proof

      let F be Function of X, Y, A be Subset of X, B be Subset of Z;

      

      thus ( [:F, ( id Z):] .: [:A, B:]) = [:(F .: A), (( id Z) .: B):] by FUNCT_3: 72

      .= [:(F .: A), B:] by FUNCT_1: 92;

    end;

    theorem :: EQREL_1:60

    for F be Function of X, Y, y be Element of Y, z be Element of Z holds ( [:F, ( id Z):] " { [y, z]}) = [:(F " {y}), {z}:]

    proof

      let F be Function of X, Y, y be Element of Y, z be Element of Z;

      

      thus ( [:F, ( id Z):] " { [y, z]}) = ( [:F, ( id Z):] " [: {y}, {z}:]) by ZFMISC_1: 29

      .= [:(F " {y}), (( id Z) " {z}):] by FUNCT_3: 73

      .= [:(F " {y}), {z}:] by FUNCT_2: 94;

    end;

    theorem :: EQREL_1:61

    for D be Subset-Family of X, A be Subset of D holds ( union A) is Subset of X

    proof

      let D be Subset-Family of X, A be Subset of D;

      ( union A) c= X

      proof

        let e be object;

        assume e in ( union A);

        then ex u be set st e in u & u in A by TARSKI:def 4;

        then e in ( union D) by TARSKI:def 4;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: EQREL_1:62

    for X be set, D be a_partition of X, A,B be Subset of D holds ( union (A /\ B)) = (( union A) /\ ( union B))

    proof

      let X be set, D be a_partition of X, A,B be Subset of D;

      thus ( union (A /\ B)) c= (( union A) /\ ( union B)) by ZFMISC_1: 79;

      let e be object;

      assume

       A1: e in (( union A) /\ ( union B));

      then e in ( union A) by XBOOLE_0:def 4;

      then

      consider a be set such that

       A2: e in a and

       A3: a in A by TARSKI:def 4;

      

       A4: a in D by A3;

      e in ( union B) by A1, XBOOLE_0:def 4;

      then

      consider b be set such that

       A5: e in b and

       A6: b in B by TARSKI:def 4;

      

       A7: b in D by A6;

       not a misses b by A2, A5, XBOOLE_0: 3;

      then a = b by A4, A7, Def4;

      then a in (A /\ B) by A3, A6, XBOOLE_0:def 4;

      hence thesis by A2, TARSKI:def 4;

    end;

    theorem :: EQREL_1:63

    for D be a_partition of X, A be Subset of D, B be Subset of X st B = ( union A) holds (B ` ) = ( union (A ` ))

    proof

      let D be a_partition of X, A be Subset of D, B be Subset of X;

      assume

       A1: B = ( union A);

      ( union D) = X by Def4;

      hence (B ` ) c= ( union (A ` )) by A1, Th55;

      let e be object;

      assume e in ( union (A ` ));

      then

      consider u be set such that

       A2: e in u and

       A3: u in (A ` ) by TARSKI:def 4;

      

       A4: u in D by A3;

      assume not e in (B ` );

      then e in B by A2, A4, SUBSET_1: 29;

      then

      consider v be set such that

       A5: e in v and

       A6: v in A by A1, TARSKI:def 4;

      

       A7: v in D by A6;

       not u misses v by A2, A5, XBOOLE_0: 3;

      then u = v by A4, A7, Def4;

      hence contradiction by A3, A6, XBOOLE_0:def 5;

    end;

    theorem :: EQREL_1:64

    for E be Equivalence_Relation of X holds ( Class E) is non empty;

    definition

      let X;

      let D be non empty a_partition of X;

      :: EQREL_1:def9

      func proj D -> Function of X, D means

      : Def9: for p be Element of X holds p in (it . p);

      existence

      proof

        defpred P[ object, object] means ex A be set st A = $2 & $1 in A;

         A1:

        now

          

           A2: ( union D) = X by Def4;

          let e be object;

          assume e in X;

          then ex u be set st e in u & u in D by A2, TARSKI:def 4;

          hence ex u be object st u in D & P[e, u];

        end;

        consider F be Function of X, D such that

         A3: for e be object st e in X holds P[e, (F . e)] from FUNCT_2:sch 1( A1);

        take F;

        let p be Element of X;

         P[p, (F . p)] by A3;

        hence thesis;

      end;

      correctness

      proof

        let F,G be Function of X, D such that

         A4: (for p be Element of X holds p in (F . p)) & for p be Element of X holds p in (G . p);

        now

          let x be Element of X;

          x in (F . x) & x in (G . x) by A4;

          then

           A5: not (F . x) misses (G . x) by XBOOLE_0: 3;

          (F . x) is Subset of X & (G . x) is Subset of X by TARSKI:def 3;

          hence (F . x) = (G . x) by A5, Def4;

        end;

        hence F = G by FUNCT_2: 63;

      end;

    end

    theorem :: EQREL_1:65

    

     Th65: for D be non empty a_partition of X, p be Element of X, A be Element of D st p in A holds A = (( proj D) . p)

    proof

      let D be non empty a_partition of X, p be Element of X, A be Element of D such that

       A1: p in A;

      p in (( proj D) . p) by Def9;

      then (( proj D) . p) is Subset of X & not (( proj D) . p) misses A by A1, TARSKI:def 3, XBOOLE_0: 3;

      hence thesis by Def4;

    end;

    theorem :: EQREL_1:66

    for D be non empty a_partition of X, p be Element of D holds p = (( proj D) " {p})

    proof

      let D be non empty a_partition of X, p be Element of D;

      thus p c= (( proj D) " {p})

      proof

        let e be object;

        assume

         A1: e in p;

        then (( proj D) . e) = p by Th65;

        then (( proj D) . e) in {p} by TARSKI:def 1;

        hence thesis by A1, FUNCT_2: 38;

      end;

      let e be object;

      assume

       A2: e in (( proj D) " {p});

      then (( proj D) . e) in {p} by FUNCT_1:def 7;

      then (( proj D) . e) = p by TARSKI:def 1;

      hence e in p by A2, Def9;

    end;

    theorem :: EQREL_1:67

    for D be non empty a_partition of X, A be Subset of D holds (( proj D) " A) = ( union A)

    proof

      let D be non empty a_partition of X, A be Subset of D;

      thus (( proj D) " A) c= ( union A)

      proof

        let e be object;

        assume e in (( proj D) " A);

        then (( proj D) . e) in A & e in (( proj D) . e) by Def9, FUNCT_2: 38;

        hence thesis by TARSKI:def 4;

      end;

      let e be object;

      assume e in ( union A);

      then

      consider u be set such that

       A1: e in u and

       A2: u in A by TARSKI:def 4;

      

       A3: u in D by A2;

      then (( proj D) . e) = u by A1, Th65;

      hence thesis by A1, A2, A3, FUNCT_2: 38;

    end;

    theorem :: EQREL_1:68

    for D be non empty a_partition of X, W be Element of D holds ex W9 be Element of X st (( proj D) . W9) = W

    proof

      let D be non empty a_partition of X, W be Element of D;

      reconsider p = W as Subset of X;

      p <> {} by Def4;

      then

      consider W9 be Element of X such that

       A1: W9 in p by SUBSET_1: 4;

      take W9;

      thus thesis by A1, Th65;

    end;

    theorem :: EQREL_1:69

    for D be non empty a_partition of X, W be Subset of X st for B be Subset of X st B in D & B meets W holds B c= W holds W = (( proj D) " (( proj D) .: W))

    proof

      let D be non empty a_partition of X, W be Subset of X such that

       A1: for B be Subset of X st B in D & B meets W holds B c= W;

      W c= X;

      then W c= ( dom ( proj D)) by FUNCT_2:def 1;

      hence W c= (( proj D) " (( proj D) .: W)) by FUNCT_1: 76;

      let e be object;

      assume

       A2: e in (( proj D) " (( proj D) .: W));

      then

      reconsider d = e as Element of X;

      (( proj D) . e) in (( proj D) .: W) by A2, FUNCT_1:def 7;

      then

      consider c be Element of X such that

       A3: c in W and

       A4: (( proj D) . d) = (( proj D) . c) by FUNCT_2: 65;

      reconsider B = (( proj D) . c) as Subset of X by TARSKI:def 3;

      c in (( proj D) . c) by Def9;

      then B meets W by A3, XBOOLE_0: 3;

      then

       A5: B c= W by A1;

      d in B by A4, Def9;

      hence thesis by A5;

    end;

    theorem :: EQREL_1:70

    for X be set, P be a_partition of X, x,a,b be set st x in a & a in P & x in b & b in P holds a = b by Def4, XBOOLE_0: 3;