msualg_5.miz



    begin

    reserve I,X,x,d,i for set;

    reserve M for ManySortedSet of I;

    reserve EqR1,EqR2 for Equivalence_Relation of X;

    definition

      let X be set, R be Relation of X;

      :: MSUALG_5:def1

      func EqCl R -> Equivalence_Relation of X means

      : Def1: R c= it & for EqR2 be Equivalence_Relation of X st R c= EqR2 holds it c= EqR2;

      existence by EQREL_1: 12;

      uniqueness

      proof

        let C1,C2 be Equivalence_Relation of X such that

         A1: R c= C1 and

         A2: for EqR2 be Equivalence_Relation of X st R c= EqR2 holds C1 c= EqR2 and

         A3: R c= C2 and

         A4: for EqR2 be Equivalence_Relation of X st R c= EqR2 holds C2 c= EqR2;

        

         A5: C2 c= C1 by A1, A4;

        C1 c= C2 by A2, A3;

        hence C1 = C2 by A5, XBOOLE_0:def 10;

      end;

    end

    theorem :: MSUALG_5:1

    

     Th1: (EqR1 "\/" EqR2) = ( EqCl (EqR1 \/ EqR2))

    proof

      

       A1: for EqR3 be Equivalence_Relation of X st (EqR1 \/ EqR2) c= EqR3 holds (EqR1 "\/" EqR2) c= EqR3 by EQREL_1:def 2;

      (EqR1 \/ EqR2) c= (EqR1 "\/" EqR2) by EQREL_1:def 2;

      hence thesis by A1, Def1;

    end;

    theorem :: MSUALG_5:2

    

     Th2: ( EqCl EqR1) = EqR1

    proof

      for EqR2 be Equivalence_Relation of X st EqR1 c= EqR2 holds EqR1 c= EqR2;

      hence thesis by Def1;

    end;

    begin

    definition

      let X be set;

      :: MSUALG_5:def2

      func EqRelLatt X -> strict Lattice means

      : Def2: the carrier of it = { x where x be Relation of X, X : x is Equivalence_Relation of X } & for x,y be Equivalence_Relation of X holds (the L_meet of it . (x,y)) = (x /\ y) & (the L_join of it . (x,y)) = (x "\/" y);

      existence

      proof

        set B = { x where x be Relation of X, X : x is Equivalence_Relation of X };

        ( id X) in B;

        then

        reconsider B as non empty set;

        defpred Z[ Element of B, Element of B, Element of B] means (($1 \/ $2) c= $3 & for x9 be Element of B st ($1 \/ $2) c= x9 holds $3 c= x9);

        

         A1: for x,y be Element of B holds ex z be Element of B st Z[x, y, z]

        proof

          let x,y be Element of B;

          y in B;

          then

           A2: ex y99 be Relation of X, X st y = y99 & y99 is Equivalence_Relation of X;

          x in B;

          then ex x99 be Relation of X, X st x = x99 & x99 is Equivalence_Relation of X;

          then

          reconsider x1 = x, y1 = y as Equivalence_Relation of X by A2;

          consider z be Equivalence_Relation of X such that

           A3: (x1 \/ y1) c= z and

           A4: for x9 be Equivalence_Relation of X st (x1 \/ y1) c= x9 holds z c= x9 by EQREL_1: 12;

          z in B;

          then

          reconsider z9 = z as Element of B;

          take z9;

          thus (x \/ y) c= z9 by A3;

          hereby

            let x9 be Element of B such that

             A5: (x \/ y) c= x9;

            x9 in B;

            then ex x99 be Relation of X, X st x9 = x99 & x99 is Equivalence_Relation of X;

            then

            reconsider x19 = x9 as Equivalence_Relation of X;

            (x \/ y) c= x19 by A5;

            hence z9 c= x9 by A4;

          end;

        end;

        consider B1 be BinOp of B such that

         A6: for x,y be Element of B holds Z[x, y, (B1 . (x,y))] from BINOP_1:sch 3( A1);

        defpred Z[ Element of B, Element of B, Element of B] means $3 = ($1 /\ $2);

        

         A7: for x,y be Element of B holds ex z be Element of B st Z[x, y, z]

        proof

          let x,y be Element of B;

          y in B;

          then

           A8: ex y1 be Relation of X, X st y = y1 & y1 is Equivalence_Relation of X;

          x in B;

          then ex x1 be Relation of X, X st x = x1 & x1 is Equivalence_Relation of X;

          then

          reconsider x9 = x, y9 = y as Equivalence_Relation of X by A8;

          set z = (x9 /\ y9);

          z in B;

          then

          reconsider z as Element of B;

          take z;

          thus thesis;

        end;

        consider B2 be BinOp of B such that

         A9: for x,y be Element of B holds Z[x, y, (B2 . (x,y))] from BINOP_1:sch 3( A7);

        reconsider L = LattStr (# B, B1, B2 #) as non empty LattStr;

         A10:

        now

          let x,y be Equivalence_Relation of X;

          

           A11: y in B;

          x in B;

          then

          reconsider x1 = x, y1 = y as Element of B by A11;

          reconsider B19 = (B1 . (x1,y1)) as Element of B;

          B19 in B;

          then ex B199 be Relation of X, X st B19 = B199 & B199 is Equivalence_Relation of X;

          then

          reconsider B19 as Equivalence_Relation of X;

          

           A12: for x9 be Element of B st (x1 \/ y1) c= x9 holds (B1 . (x1,y1)) c= x9 by A6;

           A13:

          now

            let x9 be Equivalence_Relation of X such that

             A14: (x \/ y) c= x9;

            x9 in B;

            then

            reconsider x19 = x9 as Element of B;

            (x \/ y) c= x19 by A14;

            hence (B1 . (x,y)) c= x9 by A12;

          end;

          (x1 \/ y1) c= (B1 . (x1,y1)) by A6;

          then B19 = (x "\/" y) by A13, EQREL_1:def 2;

          hence (B1 . (x,y)) = (x "\/" y);

        end;

         A15:

        now

          let a,b,c be Element of B;

          b in B;

          then

           A16: ex x2 be Relation of X, X st b = x2 & x2 is Equivalence_Relation of X;

          c in B;

          then

           A17: ex x3 be Relation of X, X st c = x3 & x3 is Equivalence_Relation of X;

          a in B;

          then ex x1 be Relation of X, X st a = x1 & x1 is Equivalence_Relation of X;

          then

          reconsider U1 = a, U2 = b, U3 = c as Equivalence_Relation of X by A16, A17;

          

          thus (B1 . (a,(B1 . (b,c)))) = (B1 . (a,(U2 "\/" U3))) by A10

          .= (U1 "\/" (U2 "\/" U3)) by A10

          .= ((U1 "\/" U2) "\/" U3) by EQREL_1: 13

          .= (B1 . ((U1 "\/" U2),c)) by A10

          .= (B1 . ((B1 . (a,b)),c)) by A10;

        end;

        

         A18: for a,b,c be Element of L holds (a "\/" (b "\/" c)) = ((a "\/" b) "\/" c)

        proof

          let a,b,c be Element of L;

          reconsider x = a, y = b, z = c as Element of B;

          

           A19: (the L_join of L . (a,b)) = (a "\/" b) by LATTICES:def 1;

          

          thus (a "\/" (b "\/" c)) = (the L_join of L . (a,(b "\/" c))) by LATTICES:def 1

          .= (B1 . (x,(B1 . (y,z)))) by LATTICES:def 1

          .= (the L_join of L . ((the L_join of L . (a,b)),c)) by A15

          .= ((a "\/" b) "\/" c) by A19, LATTICES:def 1;

        end;

         A20:

        now

          let a,b be Element of B;

          b in B;

          then

           A21: ex x2 be Relation of X, X st b = x2 & x2 is Equivalence_Relation of X;

          a in B;

          then ex x1 be Relation of X, X st a = x1 & x1 is Equivalence_Relation of X;

          then

          reconsider U1 = a, U2 = b as Equivalence_Relation of X by A21;

          

          thus (B1 . (a,b)) = (U2 "\/" U1) by A10

          .= (B1 . (b,a)) by A10;

        end;

        

         A22: for a,b be Element of L holds (a "\/" b) = (b "\/" a)

        proof

          let a,b be Element of L;

          reconsider x = a, y = b as Element of B;

          

          thus (a "\/" b) = (B1 . (x,y)) by LATTICES:def 1

          .= (the L_join of L . (b,a)) by A20

          .= (b "\/" a) by LATTICES:def 1;

        end;

         A23:

        now

          let x,y be Equivalence_Relation of X;

          

           A24: y in B;

          x in B;

          then

          reconsider x9 = x, y9 = y as Element of B by A24;

          (B2 . (x9,y9)) = (x9 /\ y9) by A9;

          hence (B2 . (x,y)) = (x /\ y);

        end;

         A25:

        now

          let a,b,c be Element of B;

          b in B;

          then

           A26: ex x2 be Relation of X, X st b = x2 & x2 is Equivalence_Relation of X;

          c in B;

          then

           A27: ex x3 be Relation of X, X st c = x3 & x3 is Equivalence_Relation of X;

          a in B;

          then ex x1 be Relation of X, X st a = x1 & x1 is Equivalence_Relation of X;

          then

          reconsider U1 = a, U2 = b, U3 = c as Equivalence_Relation of X by A26, A27;

          

          thus (B2 . (a,(B2 . (b,c)))) = (B2 . (a,(U2 /\ U3))) by A23

          .= (U1 /\ (U2 /\ U3)) by A23

          .= ((U1 /\ U2) /\ U3) by XBOOLE_1: 16

          .= (B2 . ((U1 /\ U2),c)) by A23

          .= (B2 . ((B2 . (a,b)),c)) by A23;

        end;

        

         A28: for a,b,c be Element of L holds (a "/\" (b "/\" c)) = ((a "/\" b) "/\" c)

        proof

          let a,b,c be Element of L;

          reconsider x = a, y = b, z = c as Element of B;

          

           A29: (the L_meet of L . (a,b)) = (a "/\" b) by LATTICES:def 2;

          

          thus (a "/\" (b "/\" c)) = (the L_meet of L . (a,(b "/\" c))) by LATTICES:def 2

          .= (B2 . (x,(B2 . (y,z)))) by LATTICES:def 2

          .= (the L_meet of L . ((the L_meet of L . (a,b)),c)) by A25

          .= ((a "/\" b) "/\" c) by A29, LATTICES:def 2;

        end;

        

         A30: for a,b be Element of L holds (a "/\" (a "\/" b)) = a

        proof

          let a,b be Element of L;

          reconsider x = a, y = b as Element of B;

          

           A31: (B2 . (x,(B1 . (x,y)))) = x

          proof

            y in B;

            then

             A32: ex x2 be Relation of X, X st y = x2 & x2 is Equivalence_Relation of X;

            x in B;

            then ex x1 be Relation of X, X st x = x1 & x1 is Equivalence_Relation of X;

            then

            reconsider U1 = x, U2 = y as Equivalence_Relation of X by A32;

            (B1 . (x,y)) = (U1 "\/" U2) by A10;

            

            hence (B2 . (x,(B1 . (x,y)))) = (U1 /\ (U1 "\/" U2)) by A23

            .= x by EQREL_1: 16;

          end;

          

          thus (a "/\" (a "\/" b)) = (the L_meet of L . (a,(a "\/" b))) by LATTICES:def 2

          .= a by A31, LATTICES:def 1;

        end;

         A33:

        now

          let a,b be Element of B;

          b in B;

          then

           A34: ex x2 be Relation of X, X st b = x2 & x2 is Equivalence_Relation of X;

          a in B;

          then ex x1 be Relation of X, X st a = x1 & x1 is Equivalence_Relation of X;

          then

          reconsider U1 = a, U2 = b as Equivalence_Relation of X by A34;

          

          thus (B2 . (a,b)) = (U2 /\ U1) by A23

          .= (B2 . (b,a)) by A23;

        end;

        

         A35: for a,b be Element of L holds (a "/\" b) = (b "/\" a)

        proof

          let a,b be Element of L;

          reconsider x = a, y = b as Element of B;

          

          thus (a "/\" b) = (B2 . (x,y)) by LATTICES:def 2

          .= (the L_meet of L . (b,a)) by A33

          .= (b "/\" a) by LATTICES:def 2;

        end;

        for a,b be Element of L holds ((a "/\" b) "\/" b) = b

        proof

          let a,b be Element of L;

          reconsider x = a, y = b as Element of B;

          

           A36: (B1 . ((B2 . (x,y)),y)) = y

          proof

            y in B;

            then

             A37: ex x2 be Relation of X, X st y = x2 & x2 is Equivalence_Relation of X;

            x in B;

            then ex x1 be Relation of X, X st x = x1 & x1 is Equivalence_Relation of X;

            then

            reconsider U1 = x, U2 = y as Equivalence_Relation of X by A37;

            (B2 . (x,y)) = (U1 /\ U2) by A23;

            

            hence (B1 . ((B2 . (x,y)),y)) = (U2 "\/" (U1 /\ U2)) by A10

            .= y by EQREL_1: 17;

          end;

          

          thus ((a "/\" b) "\/" b) = (the L_join of L . ((a "/\" b),b)) by LATTICES:def 1

          .= b by A36, LATTICES:def 2;

        end;

        then L is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing by A22, A18, A35, A28, A30, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;

        then

        reconsider L as strict Lattice;

        take L;

        thus the carrier of L = { x where x be Relation of X, X : x is Equivalence_Relation of X };

        thus thesis by A10, A23;

      end;

      uniqueness

      proof

        let P1,P2 be strict Lattice such that

         A38: the carrier of P1 = { x where x be Relation of X, X : x is Equivalence_Relation of X } and

         A39: for x,y be Equivalence_Relation of X holds (the L_meet of P1 . (x,y)) = (x /\ y) & (the L_join of P1 . (x,y)) = (x "\/" y) and

         A40: the carrier of P2 = { x where x be Relation of X, X : x is Equivalence_Relation of X } and

         A41: for x,y be Equivalence_Relation of X holds (the L_meet of P2 . (x,y)) = (x /\ y) & (the L_join of P2 . (x,y)) = (x "\/" y);

        reconsider Z = the carrier of P1 as non empty set;

        now

          let x,y be Element of Z;

          y in Z;

          then

           A42: ex x3 be Relation of X, X st y = x3 & x3 is Equivalence_Relation of X by A38;

          x in Z;

          then ex x2 be Relation of X, X st x = x2 & x2 is Equivalence_Relation of X by A38;

          then

          reconsider x1 = x, y1 = y as Equivalence_Relation of X by A42;

          

          thus (the L_meet of P1 . (x,y)) = (x1 /\ y1) by A39

          .= (the L_meet of P2 . (x,y)) by A41;

        end;

        then

         A43: the L_meet of P1 = the L_meet of P2 by A38, A40, BINOP_1: 2;

        now

          let x,y be Element of Z;

          y in Z;

          then

           A44: ex x3 be Relation of X, X st y = x3 & x3 is Equivalence_Relation of X by A38;

          x in Z;

          then ex x2 be Relation of X, X st x = x2 & x2 is Equivalence_Relation of X by A38;

          then

          reconsider x1 = x, y1 = y as Equivalence_Relation of X by A44;

          

          thus (the L_join of P1 . (x,y)) = (x1 "\/" y1) by A39

          .= (the L_join of P2 . (x,y)) by A41;

        end;

        hence thesis by A38, A40, A43, BINOP_1: 2;

      end;

    end

    begin

    registration

      let I, M;

      cluster MSEquivalence_Relation-like for ManySortedRelation of M;

      existence

      proof

        deffunc F( object) = ( id (M . $1));

        consider f be ManySortedSet of I such that

         A1: for d be object st d in I holds (f . d) = F(d) from PBOOLE:sch 4;

        for i be set st i in I holds (f . i) is Relation of (M . i), (M . i)

        proof

          let i be set;

          assume i in I;

          then (f . i) = ( id (M . i)) by A1;

          hence thesis;

        end;

        then

        reconsider f as ManySortedRelation of M by MSUALG_4:def 1;

        take f;

        for i be set, R be Relation of (M . i) st i in I & (f . i) = R holds R is Equivalence_Relation of (M . i)

        proof

          let i be set, R be Relation of (M . i);

          assume that

           A2: i in I and

           A3: (f . i) = R;

          R = ( id (M . i)) by A1, A2, A3;

          hence thesis;

        end;

        hence thesis by MSUALG_4:def 2;

      end;

    end

    definition

      let I, M;

      mode Equivalence_Relation of M is MSEquivalence_Relation-like ManySortedRelation of M;

    end

    reserve I for non empty set;

    reserve M for ManySortedSet of I;

    reserve EqR,EqR1,EqR2,EqR3,EqR4 for Equivalence_Relation of M;

    definition

      let I be non empty set;

      let M be ManySortedSet of I, R be ManySortedRelation of M;

      :: MSUALG_5:def3

      func EqCl R -> Equivalence_Relation of M means

      : Def3: for i be Element of I holds (it . i) = ( EqCl (R . i));

      existence

      proof

        deffunc F( Element of I) = ( EqCl (R . $1));

        consider EqR be ManySortedSet of I such that

         A1: for i be Element of I holds (EqR . i) = F(i) from PBOOLE:sch 5;

        for i be set st i in I holds (EqR . i) is Relation of (M . i)

        proof

          let i be set;

          assume i in I;

          then

          reconsider i9 = i as Element of I;

          (EqR . i) = ( EqCl (R . i9)) by A1;

          hence thesis;

        end;

        then

        reconsider EqR as ManySortedRelation of M by MSUALG_4:def 1;

        for i be set, R be Relation of (M . i) st i in I & (EqR . i) = R holds R is Equivalence_Relation of (M . i)

        proof

          let i be set;

          let R1 be Relation of (M . i);

          assume that

           A2: i in I and

           A3: (EqR . i) = R1;

          reconsider i9 = i as Element of I by A2;

          R1 = ( EqCl (R . i9)) by A1, A3;

          hence thesis;

        end;

        then

        reconsider EqR as Equivalence_Relation of M by MSUALG_4:def 2;

        take EqR;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let C1,C2 be Equivalence_Relation of M such that

         A4: for i be Element of I holds (C1 . i) = ( EqCl (R . i)) and

         A5: for i be Element of I holds (C2 . i) = ( EqCl (R . i));

        now

          let i be object;

          assume i in I;

          then

          reconsider i1 = i as Element of I;

          

          thus (C1 . i) = ( EqCl (R . i1)) by A4

          .= (C2 . i) by A5;

        end;

        hence C1 = C2 by PBOOLE: 3;

      end;

    end

    theorem :: MSUALG_5:3

    ( EqCl EqR) = EqR

    proof

      now

        let i be Element of I;

        reconsider ER = (EqR . i) as Equivalence_Relation of (M . i) by MSUALG_4:def 2;

        

        thus (EqR . i) = ( EqCl ER) by Th2

        .= ( EqCl (EqR . i));

      end;

      hence thesis by Def3;

    end;

    begin

    definition

      let I be non empty set, M be ManySortedSet of I;

      let EqR1,EqR2 be Equivalence_Relation of M;

      :: MSUALG_5:def4

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

      : Def4: ex EqR3 be ManySortedRelation of M st EqR3 = (EqR1 (\/) EqR2) & it = ( EqCl EqR3);

      existence

      proof

        deffunc F( object) = ((EqR1 (\/) EqR2) . $1);

        consider E be ManySortedSet of I such that

         A1: for i be object st i in I holds (E . i) = F(i) from PBOOLE:sch 4;

        for i be set st i in I holds (E . i) is Relation of (M . i)

        proof

          let i be set;

          assume

           A2: i in I;

          then

          reconsider i9 = i as Element of I;

          (E . i) = ((EqR1 (\/) EqR2) . i) by A1, A2

          .= ((EqR1 . i9) \/ (EqR2 . i9)) by PBOOLE:def 4;

          hence thesis;

        end;

        then

        reconsider E as ManySortedRelation of M by MSUALG_4:def 1;

        take ( EqCl E);

        take E;

        thus thesis by A1, PBOOLE: 3;

      end;

      uniqueness ;

      commutativity ;

    end

    theorem :: MSUALG_5:4

    

     Th4: (EqR1 (\/) EqR2) c= (EqR1 "\/" EqR2)

    proof

      consider EqR3 be ManySortedRelation of M such that

       A1: EqR3 = (EqR1 (\/) EqR2) and

       A2: (EqR1 "\/" EqR2) = ( EqCl EqR3) by Def4;

      now

        let i be object;

        assume i in I;

        then

        reconsider i9 = i as Element of I;

        (EqR3 . i) c= ( EqCl (EqR3 . i9)) by Def1;

        hence (EqR3 . i) c= ((EqR1 "\/" EqR2) . i) by A2, Def3;

      end;

      hence thesis by A1, PBOOLE:def 2;

    end;

    theorem :: MSUALG_5:5

    

     Th5: for EqR be Equivalence_Relation of M st (EqR1 (\/) EqR2) c= EqR holds (EqR1 "\/" EqR2) c= EqR

    proof

      consider EqR3 be ManySortedRelation of M such that

       A1: EqR3 = (EqR1 (\/) EqR2) and

       A2: (EqR1 "\/" EqR2) = ( EqCl EqR3) by Def4;

      let EqR be Equivalence_Relation of M such that

       A3: (EqR1 (\/) EqR2) c= EqR;

      now

        let i be object;

        assume

         A4: i in I;

        then

        reconsider i9 = i as Element of I;

        (EqR . i9) is Relation of (M . i);

        then

        reconsider E = (EqR . i) as Equivalence_Relation of (M . i) by MSUALG_4:def 2;

        (EqR3 . i) c= E by A3, A1, A4, PBOOLE:def 2;

        then ( EqCl (EqR3 . i9)) c= E by Def1;

        hence ((EqR1 "\/" EqR2) . i) c= (EqR . i) by A2, Def3;

      end;

      hence thesis by PBOOLE:def 2;

    end;

    theorem :: MSUALG_5:6

    

     Th6: ((EqR1 (\/) EqR2) c= EqR3 & for EqR be Equivalence_Relation of M st (EqR1 (\/) EqR2) c= EqR holds EqR3 c= EqR) implies EqR3 = (EqR1 "\/" EqR2)

    proof

      assume that

       A1: (EqR1 (\/) EqR2) c= EqR3 and

       A2: for EqR be Equivalence_Relation of M st (EqR1 (\/) EqR2) c= EqR holds EqR3 c= EqR;

      

       A3: (EqR1 "\/" EqR2) c= EqR3 by A1, Th5;

      EqR3 c= (EqR1 "\/" EqR2) by A2, Th4;

      hence thesis by A3, PBOOLE: 146;

    end;

    theorem :: MSUALG_5:7

    (EqR "\/" EqR) = EqR

    proof

      for EqR3 st (EqR (\/) EqR) c= EqR3 holds EqR c= EqR3;

      hence thesis by Th6;

    end;

    theorem :: MSUALG_5:8

    

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

    proof

      for EqR4 holds EqR4 = (EqR1 "\/" (EqR2 "\/" EqR3)) implies ((EqR1 "\/" EqR2) "\/" EqR3) c= EqR4

      proof

        let EqR4;

        

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

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

        then

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

        (EqR2 "\/" EqR3) c= (EqR1 (\/) (EqR2 "\/" EqR3)) by PBOOLE: 14;

        then (EqR2 "\/" EqR3) c= EqR4 by A2, PBOOLE: 13;

        then

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

        EqR2 c= (EqR2 (\/) EqR3) by PBOOLE: 14;

        then

         A4: EqR2 c= EqR4 by A3, PBOOLE: 13;

        EqR1 c= (EqR1 (\/) (EqR2 "\/" EqR3)) by PBOOLE: 14;

        then EqR1 c= EqR4 by A2, PBOOLE: 13;

        then (EqR1 (\/) EqR2) c= EqR4 by A4, PBOOLE: 16;

        then

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

        EqR3 c= (EqR2 (\/) EqR3) by PBOOLE: 14;

        then EqR3 c= EqR4 by A3, PBOOLE: 13;

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

        hence thesis by Th5;

      end;

      then

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

      for EqR4 holds EqR4 = ((EqR1 "\/" EqR2) "\/" EqR3) implies (EqR1 "\/" (EqR2 "\/" EqR3)) c= EqR4

      proof

        let EqR4;

        

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

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

        then

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

        (EqR1 "\/" EqR2) c= ((EqR1 "\/" EqR2) (\/) EqR3) by PBOOLE: 14;

        then (EqR1 "\/" EqR2) c= EqR4 by A8, PBOOLE: 13;

        then

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

        EqR3 c= ((EqR1 "\/" EqR2) (\/) EqR3) by PBOOLE: 14;

        then

         A10: EqR3 c= EqR4 by A8, PBOOLE: 13;

        EqR2 c= (EqR1 (\/) EqR2) by PBOOLE: 14;

        then EqR2 c= EqR4 by A9, PBOOLE: 13;

        then (EqR2 (\/) EqR3) c= EqR4 by A10, PBOOLE: 16;

        then

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

        EqR1 c= (EqR1 (\/) EqR2) by PBOOLE: 14;

        then EqR1 c= EqR4 by A9, PBOOLE: 13;

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

        hence thesis by Th5;

      end;

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

      hence thesis by A6, PBOOLE: 146;

    end;

    theorem :: MSUALG_5:9

    

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

    proof

      

       A1: (EqR1 (/\) (EqR1 "\/" EqR2)) c= EqR1 by PBOOLE: 15;

      

       A2: EqR1 c= (EqR1 (\/) EqR2) by PBOOLE: 14;

      (EqR1 (\/) EqR2) c= (EqR1 "\/" EqR2) by Th4;

      then EqR1 c= (EqR1 "\/" EqR2) by A2, PBOOLE: 13;

      then EqR1 c= (EqR1 (/\) (EqR1 "\/" EqR2)) by PBOOLE: 17;

      hence thesis by A1, PBOOLE: 146;

    end;

    theorem :: MSUALG_5:10

    

     Th10: for EqR be Equivalence_Relation of M st EqR = (EqR1 (/\) EqR2) holds (EqR1 "\/" EqR) = EqR1

    proof

      

       A1: EqR1 = (EqR1 (\/) (EqR1 (/\) EqR2)) by PBOOLE: 31;

      

       A2: for EqR4 st (EqR1 (\/) (EqR1 (/\) EqR2)) c= EqR4 holds EqR1 c= EqR4 by PBOOLE: 31;

      let EqR be Equivalence_Relation of M;

      assume EqR = (EqR1 (/\) EqR2);

      hence thesis by A1, A2, Th6;

    end;

    theorem :: MSUALG_5:11

    

     Th11: for EqR1,EqR2 be Equivalence_Relation of M holds (EqR1 (/\) EqR2) is Equivalence_Relation of M

    proof

      let EqR1,EqR2 be Equivalence_Relation of M;

      for i be set st i in I holds ((EqR1 (/\) EqR2) . i) is Relation of (M . i), (M . i)

      proof

        let i be set;

        assume

         A1: i in I;

        then

        reconsider U19 = (EqR1 . i) as Relation of (M . i), (M . i) by MSUALG_4:def 1;

        reconsider U29 = (EqR2 . i) as Relation of (M . i), (M . i) by A1, MSUALG_4:def 1;

        ((EqR1 (/\) EqR2) . i) = (U19 /\ U29) by A1, PBOOLE:def 5;

        hence thesis;

      end;

      then

      reconsider U3 = (EqR1 (/\) EqR2) as ManySortedRelation of M by MSUALG_4:def 1;

      for i be set, R be Relation of (M . i) st i in I & (U3 . i) = R holds R is Equivalence_Relation of (M . i)

      proof

        let i be set;

        let R be Relation of (M . i);

        assume that

         A2: i in I and

         A3: (U3 . i) = R;

        reconsider U29 = (EqR2 . i) as Relation of (M . i) by A2, MSUALG_4:def 1;

        reconsider U29 as Equivalence_Relation of (M . i) by A2, MSUALG_4:def 2;

        reconsider U19 = (EqR1 . i) as Relation of (M . i) by A2, MSUALG_4:def 1;

        reconsider U19 as Equivalence_Relation of (M . i) by A2, MSUALG_4:def 2;

        (U19 /\ U29) is Equivalence_Relation of (M . i);

        hence thesis by A2, A3, PBOOLE:def 5;

      end;

      hence thesis by MSUALG_4:def 2;

    end;

    definition

      let I be non empty set;

      let M be ManySortedSet of I;

      :: MSUALG_5:def5

      func EqRelLatt M -> strict Lattice means

      : Def5: (for x be set holds x in the carrier of it iff x is Equivalence_Relation of M) & for x,y be Equivalence_Relation of M holds (the L_meet of it . (x,y)) = (x (/\) y) & (the L_join of it . (x,y)) = (x "\/" y);

      existence

      proof

        set f = the Equivalence_Relation of M;

        defpred P[ object] means $1 is Equivalence_Relation of M;

        deffunc F( Element of I) = ( bool [:(M . $1), (M . $1):]);

        consider M2 be ManySortedSet of I such that

         A1: for i be Element of I holds (M2 . i) = F(i) from PBOOLE:sch 5;

        consider B be set such that

         A2: for x be object holds x in B iff x in ( product M2) & P[x] from XBOOLE_0:sch 1;

        

         A3: for EqR be Equivalence_Relation of M holds EqR in ( product M2)

        proof

          let EqR be Equivalence_Relation of M;

          

           A4: for x be object st x in ( dom M2) holds (EqR . x) in (M2 . x)

          proof

            let x be object;

            assume x in ( dom M2);

            then

            reconsider x9 = x as Element of I;

            

             A5: (EqR . x9) is Subset of [:(M . x9), (M . x9):];

            (M2 . x9) = ( bool [:(M . x9), (M . x9):]) by A1;

            hence thesis by A5;

          end;

          ( dom EqR) = I by PARTFUN1:def 2

          .= ( dom M2) by PARTFUN1:def 2;

          hence thesis by A4, CARD_3: 9;

        end;

        then f in ( product M2);

        then

        reconsider B as non empty set by A2;

        defpred Z[ Element of B, Element of B, Element of B] means (for x1,y1 be Equivalence_Relation of M st x1 = $1 & y1 = $2 holds ex EqR3 be ManySortedRelation of M st EqR3 = (x1 (\/) y1) & $3 = ( EqCl EqR3));

        

         A6: for x,y be Element of B holds ex z be Element of B st Z[x, y, z]

        proof

          let x,y be Element of B;

          reconsider x9 = x, y9 = y as Equivalence_Relation of M by A2;

          set z = (x9 "\/" y9);

          z in ( product M2) by A3;

          then

          reconsider z as Element of B by A2;

          take z;

          let x1,y1 be Equivalence_Relation of M;

          assume that

           A7: x1 = x and

           A8: y1 = y;

          thus thesis by A7, A8, Def4;

        end;

        consider B1 be BinOp of B such that

         A9: for x,y be Element of B holds Z[x, y, (B1 . (x,y))] from BINOP_1:sch 3( A6);

        defpred Q[ Element of B, Element of B, Element of B] means for x1,y1 be Equivalence_Relation of M st x1 = $1 & y1 = $2 holds $3 = (x1 (/\) y1);

        

         A10: for x,y be Element of B holds ex z be Element of B st Q[x, y, z]

        proof

          let x,y be Element of B;

          reconsider x9 = x, y9 = y as Equivalence_Relation of M by A2;

          set z = (x9 (/\) y9);

          for i be set st i in I holds (z . i) is Relation of (M . i)

          proof

            let i be set;

            assume i in I;

            then

            reconsider i9 = i as Element of I;

            (z . i) = ((x9 . i9) /\ (y9 . i9)) by PBOOLE:def 5;

            hence thesis;

          end;

          then

          reconsider z as ManySortedRelation of M by MSUALG_4:def 1;

          for i be set, R be Relation of (M . i) st i in I & (z . i) = R holds R is Equivalence_Relation of (M . i)

          proof

            let i be set;

            let R be Relation of (M . i);

            assume that

             A11: i in I and

             A12: (z . i) = R;

            reconsider i9 = i as Element of I by A11;

            reconsider x199 = (x9 . i9), y199 = (y9 . i9) as Relation of (M . i);

            reconsider x99 = x199, y99 = y199 as Equivalence_Relation of (M . i) by MSUALG_4:def 2;

            R = (x99 /\ y99) by A12, PBOOLE:def 5;

            hence thesis;

          end;

          then

          reconsider z as Equivalence_Relation of M by MSUALG_4:def 2;

          z in ( product M2) by A3;

          then

          reconsider z as Element of B by A2;

          take z;

          thus thesis;

        end;

        consider B2 be BinOp of B such that

         A13: for x,y be Element of B holds Q[x, y, (B2 . (x,y))] from BINOP_1:sch 3( A10);

        reconsider L = LattStr (# B, B1, B2 #) as non empty LattStr;

         A14:

        now

          let x,y be Equivalence_Relation of M;

          

           A15: y in ( product M2) by A3;

          x in ( product M2) by A3;

          then

          reconsider x9 = x, y9 = y as Element of B by A2, A15;

          ex EqR3 be ManySortedRelation of M st EqR3 = (x (\/) y) & (B1 . (x9,y9)) = ( EqCl EqR3) by A9;

          hence (B1 . (x,y)) = (x "\/" y) by Def4;

        end;

         A16:

        now

          let a,b,c be Element of B;

          reconsider U1 = a, U2 = b, U3 = c as Equivalence_Relation of M by A2;

          

          thus (B1 . (a,(B1 . (b,c)))) = (B1 . (a,(U2 "\/" U3))) by A14

          .= (U1 "\/" (U2 "\/" U3)) by A14

          .= ((U1 "\/" U2) "\/" U3) by Th8

          .= (B1 . ((U1 "\/" U2),c)) by A14

          .= (B1 . ((B1 . (a,b)),c)) by A14;

        end;

        

         A17: for a,b,c be Element of L holds (a "\/" (b "\/" c)) = ((a "\/" b) "\/" c)

        proof

          let a,b,c be Element of L;

          reconsider x = a, y = b, z = c as Element of B;

          

           A18: (the L_join of L . (a,b)) = (a "\/" b) by LATTICES:def 1;

          

          thus (a "\/" (b "\/" c)) = (the L_join of L . (a,(b "\/" c))) by LATTICES:def 1

          .= (B1 . (x,(B1 . (y,z)))) by LATTICES:def 1

          .= (the L_join of L . ((the L_join of L . (a,b)),c)) by A16

          .= ((a "\/" b) "\/" c) by A18, LATTICES:def 1;

        end;

         A19:

        now

          let x,y be Equivalence_Relation of M;

          

           A20: y in ( product M2) by A3;

          x in ( product M2) by A3;

          then

          reconsider x9 = x, y9 = y as Element of B by A2, A20;

          

           A21: y9 = y;

          x9 = x;

          hence (B2 . (x,y)) = (x (/\) y) by A13, A21;

        end;

         A22:

        now

          let a,b,c be Element of B;

          reconsider U1 = a, U2 = b, U3 = c as Equivalence_Relation of M by A2;

          reconsider EQR1 = (U2 (/\) U3) as Equivalence_Relation of M by Th11;

          reconsider EQR2 = (U1 (/\) U2) as Equivalence_Relation of M by Th11;

          

          thus (B2 . (a,(B2 . (b,c)))) = (B2 . (a,EQR1)) by A19

          .= (U1 (/\) (U2 (/\) U3)) by A19

          .= ((U1 (/\) U2) (/\) U3) by PBOOLE: 29

          .= (B2 . (EQR2,c)) by A19

          .= (B2 . ((B2 . (a,b)),c)) by A19;

        end;

        

         A23: for a,b,c be Element of L holds (a "/\" (b "/\" c)) = ((a "/\" b) "/\" c)

        proof

          let a,b,c be Element of L;

          reconsider x = a, y = b, z = c as Element of B;

          

           A24: (the L_meet of L . (a,b)) = (a "/\" b) by LATTICES:def 2;

          

          thus (a "/\" (b "/\" c)) = (the L_meet of L . (a,(b "/\" c))) by LATTICES:def 2

          .= (B2 . (x,(B2 . (y,z)))) by LATTICES:def 2

          .= (the L_meet of L . ((the L_meet of L . (a,b)),c)) by A22

          .= ((a "/\" b) "/\" c) by A24, LATTICES:def 2;

        end;

         A25:

        now

          let a,b be Element of B;

          reconsider U1 = a, U2 = b as Equivalence_Relation of M by A2;

          

          thus (B1 . (a,b)) = (U1 "\/" U2) by A14

          .= (B1 . (b,a)) by A14;

        end;

        

         A26: for a,b be Element of L holds (a "\/" b) = (b "\/" a)

        proof

          let a,b be Element of L;

          reconsider x = a, y = b as Element of B;

          

          thus (a "\/" b) = (B1 . (x,y)) by LATTICES:def 1

          .= (the L_join of L . (b,a)) by A25

          .= (b "\/" a) by LATTICES:def 1;

        end;

        

         A27: for a,b be Element of L holds ((a "/\" b) "\/" b) = b

        proof

          let a,b be Element of L;

          reconsider x = a, y = b as Element of B;

          

           A28: (B1 . ((B2 . (x,y)),y)) = y

          proof

            reconsider U1 = x, U2 = y as Equivalence_Relation of M by A2;

            reconsider EQR = (U1 (/\) U2) as Equivalence_Relation of M by Th11;

            (B2 . (x,y)) = (U1 (/\) U2) by A19;

            

            hence (B1 . ((B2 . (x,y)),y)) = (EQR "\/" U2) by A14

            .= y by Th10;

          end;

          

          thus ((a "/\" b) "\/" b) = (the L_join of L . ((a "/\" b),b)) by LATTICES:def 1

          .= b by A28, LATTICES:def 2;

        end;

         A29:

        now

          let a,b be Element of B;

          reconsider U1 = a, U2 = b as Equivalence_Relation of M by A2;

          

          thus (B2 . (a,b)) = (U2 (/\) U1) by A19

          .= (B2 . (b,a)) by A19;

        end;

        

         A30: for a,b be Element of L holds (a "/\" b) = (b "/\" a)

        proof

          let a,b be Element of L;

          reconsider x = a, y = b as Element of B;

          

          thus (a "/\" b) = (B2 . (x,y)) by LATTICES:def 2

          .= (the L_meet of L . (b,a)) by A29

          .= (b "/\" a) by LATTICES:def 2;

        end;

        for a,b be Element of L holds (a "/\" (a "\/" b)) = a

        proof

          let a,b be Element of L;

          reconsider x = a, y = b as Element of B;

          

           A31: (B2 . (x,(B1 . (x,y)))) = x

          proof

            reconsider U1 = x, U2 = y as Equivalence_Relation of M by A2;

            (B1 . (x,y)) = (U1 "\/" U2) by A14;

            

            hence (B2 . (x,(B1 . (x,y)))) = (U1 (/\) (U1 "\/" U2)) by A19

            .= x by Th9;

          end;

          

          thus (a "/\" (a "\/" b)) = (the L_meet of L . (a,(a "\/" b))) by LATTICES:def 2

          .= a by A31, LATTICES:def 1;

        end;

        then L is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing by A26, A17, A27, A30, A23, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;

        then

        reconsider L as strict Lattice;

        take L;

        thus for x be set holds x in the carrier of L iff x is Equivalence_Relation of M by A2, A3;

        thus thesis by A14, A19;

      end;

      uniqueness

      proof

        let S1,S2 be strict Lattice such that

         A32: for x be set holds x in the carrier of S1 iff x is Equivalence_Relation of M and

         A33: for x,y be Equivalence_Relation of M holds (the L_meet of S1 . (x,y)) = (x (/\) y) & (the L_join of S1 . (x,y)) = (x "\/" y) and

         A34: for x be set holds x in the carrier of S2 iff x is Equivalence_Relation of M and

         A35: for x,y be Equivalence_Relation of M holds (the L_meet of S2 . (x,y)) = (x (/\) y) & (the L_join of S2 . (x,y)) = (x "\/" y);

        reconsider Z = the carrier of S1 as non empty set;

        now

          let x be object;

          x is Equivalence_Relation of M iff x in the carrier of S2 by A34;

          hence x in the carrier of S1 iff x in the carrier of S2 by A32;

        end;

        then

         A36: the carrier of S1 = the carrier of S2 by TARSKI: 2;

         A37:

        now

          let x,y be Element of Z;

          reconsider x1 = x, y1 = y as Equivalence_Relation of M by A32;

          

          thus (the L_meet of S1 . (x,y)) = (x1 (/\) y1) by A33

          .= (the L_meet of S2 . (x,y)) by A35;

          

          thus (the L_join of S1 . (x,y)) = (x1 "\/" y1) by A33

          .= (the L_join of S2 . (x,y)) by A35;

        end;

        then the L_meet of S1 = the L_meet of S2 by A36, BINOP_1: 2;

        hence thesis by A36, A37, BINOP_1: 2;

      end;

    end

    begin

    registration

      let S be non empty ManySortedSign;

      let A be MSAlgebra over S;

      cluster MSEquivalence-like -> MSEquivalence_Relation-like for ManySortedRelation of A;

      coherence by MSUALG_4:def 3;

    end

    reserve S for non void non empty ManySortedSign;

    reserve A for non-empty MSAlgebra over S;

    theorem :: MSUALG_5:12

    

     Th12: for o be OperSymbol of S holds for C1,C2 be MSCongruence of A holds for x1,y1 be set holds for a1,b1 be FinSequence holds [x1, y1] in ((C1 . (( the_arity_of o) /. (( len a1) + 1))) \/ (C2 . (( the_arity_of o) /. (( len a1) + 1)))) implies for x,y be Element of ( Args (o,A)) st x = ((a1 ^ <*x1*>) ^ b1) & y = ((a1 ^ <*y1*>) ^ b1) holds [(( Den (o,A)) . x), (( Den (o,A)) . y)] in ((C1 . ( the_result_sort_of o)) \/ (C2 . ( the_result_sort_of o)))

    proof

      let o be OperSymbol of S;

      let C1,C2 be MSCongruence of A;

      let x1,y1 be set;

      let a1,b1 be FinSequence;

      assume

       A1: [x1, y1] in ((C1 . (( the_arity_of o) /. (( len a1) + 1))) \/ (C2 . (( the_arity_of o) /. (( len a1) + 1))));

      let x,y be Element of ( Args (o,A));

      assume that

       A2: x = ((a1 ^ <*x1*>) ^ b1) and

       A3: y = ((a1 ^ <*y1*>) ^ b1);

      

       A4: y = (a1 ^ ( <*y1*> ^ b1)) by A3, FINSEQ_1: 32;

      

       A5: x = (a1 ^ ( <*x1*> ^ b1)) by A2, FINSEQ_1: 32;

      now

        per cases by A1, XBOOLE_0:def 3;

          suppose

           A6: [x1, y1] in (C1 . (( the_arity_of o) /. (( len a1) + 1)));

          for n be Nat st n in ( dom x) holds [(x . n), (y . n)] in (C1 . (( the_arity_of o) /. n))

          proof

            let n be Nat;

            assume

             A7: n in ( dom x);

            then

            reconsider dz = ( dom ( the_arity_of o)) as non empty set by MSUALG_3: 6;

            

             A8: n in ( dom ( the_arity_of o)) by A7, MSUALG_3: 6;

            then

             A9: n in ( dom (the Sorts of A * ( the_arity_of o))) by PARTFUN1:def 2;

            reconsider so = (the Sorts of A * ( the_arity_of o)) as non-empty ManySortedSet of dz;

            

             A10: ( product so) is non empty;

            ( pi (( Args (o,A)),n)) = ( pi ((((the Sorts of A # ) * the Arity of S) . o),n)) by MSUALG_1:def 4

            .= ( pi (((the Sorts of A # ) . (the Arity of S . o)),n)) by FUNCT_2: 15

            .= ( pi (((the Sorts of A # ) . ( the_arity_of o)),n)) by MSUALG_1:def 1

            .= ( pi (( product (the Sorts of A * ( the_arity_of o))),n)) by FINSEQ_2:def 5

            .= ((the Sorts of A * ( the_arity_of o)) . n) by A9, A10, CARD_3: 12

            .= (the Sorts of A . (( the_arity_of o) . n)) by A8, FUNCT_1: 13

            .= (the Sorts of A . (( the_arity_of o) /. n)) by A8, PARTFUN1:def 6;

            then

             A11: (x . n) in (the Sorts of A . (( the_arity_of o) /. n)) by CARD_3:def 6;

            

             A12: n in ( dom (a1 ^ <*x1*>)) or ex k be Nat st k in ( dom b1) & n = (( len (a1 ^ <*x1*>)) + k) by A2, A7, FINSEQ_1: 25;

            now

              per cases by A12, FINSEQ_1: 25;

                suppose

                 A13: n in ( dom a1);

                then

                 A14: (y . n) = (a1 . n) by A4, FINSEQ_1:def 7;

                (x . n) = (a1 . n) by A5, A13, FINSEQ_1:def 7;

                hence thesis by A11, A14, EQREL_1: 5;

              end;

                suppose ex m be Nat st m in ( dom <*x1*>) & n = (( len a1) + m);

                then

                consider m be Nat such that

                 A15: m in ( dom <*x1*>) and

                 A16: n = (( len a1) + m);

                

                 A17: m in ( Seg 1) by A15, FINSEQ_1: 38;

                then

                 A18: m = 1 by FINSEQ_1: 2, TARSKI:def 1;

                then

                 A19: n in ( Seg (( len a1) + 1)) by A16, FINSEQ_1: 4;

                then n in ( Seg (( len a1) + ( len <*y1*>))) by FINSEQ_1: 40;

                then n in ( Seg ( len (a1 ^ <*y1*>))) by FINSEQ_1: 22;

                then n in ( dom (a1 ^ <*y1*>)) by FINSEQ_1:def 3;

                

                then

                 A20: (y . n) = ((a1 ^ <*y1*>) . (( len a1) + 1)) by A3, A16, A18, FINSEQ_1:def 7

                .= y1 by FINSEQ_1: 42;

                n in ( Seg (( len a1) + ( len <*x1*>))) by A19, FINSEQ_1: 40;

                then n in ( Seg ( len (a1 ^ <*x1*>))) by FINSEQ_1: 22;

                then n in ( dom (a1 ^ <*x1*>)) by FINSEQ_1:def 3;

                

                then (x . n) = ((a1 ^ <*x1*>) . (( len a1) + 1)) by A2, A16, A18, FINSEQ_1:def 7

                .= x1 by FINSEQ_1: 42;

                hence thesis by A6, A16, A17, A20, FINSEQ_1: 2, TARSKI:def 1;

              end;

                suppose ex k be Element of NAT st k in ( dom b1) & n = (( len (a1 ^ <*x1*>)) + k);

                then

                consider k be Element of NAT such that

                 A21: k in ( dom b1) and

                 A22: n = (( len (a1 ^ <*x1*>)) + k);

                n = ((( len a1) + ( len <*x1*>)) + k) by A22, FINSEQ_1: 22;

                then n = ((( len a1) + 1) + k) by FINSEQ_1: 40;

                then n = ((( len a1) + ( len <*y1*>)) + k) by FINSEQ_1: 40;

                then n = (( len (a1 ^ <*y1*>)) + k) by FINSEQ_1: 22;

                then

                 A23: (y . n) = (b1 . k) by A3, A21, FINSEQ_1:def 7;

                (x . n) = (b1 . k) by A2, A21, A22, FINSEQ_1:def 7;

                hence thesis by A11, A23, EQREL_1: 5;

              end;

            end;

            hence thesis;

          end;

          then [(( Den (o,A)) . x), (( Den (o,A)) . y)] in (C1 . ( the_result_sort_of o)) by MSUALG_4:def 4;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose

           A24: [x1, y1] in (C2 . (( the_arity_of o) /. (( len a1) + 1)));

          for n be Nat st n in ( dom x) holds [(x . n), (y . n)] in (C2 . (( the_arity_of o) /. n))

          proof

            let n be Nat;

            assume

             A25: n in ( dom x);

            then

            reconsider dz = ( dom ( the_arity_of o)) as non empty set by MSUALG_3: 6;

            

             A26: n in ( dom ( the_arity_of o)) by A25, MSUALG_3: 6;

            then

             A27: n in ( dom (the Sorts of A * ( the_arity_of o))) by PARTFUN1:def 2;

            reconsider so = (the Sorts of A * ( the_arity_of o)) as non-empty ManySortedSet of dz;

            

             A28: ( product so) is non empty;

            ( pi (( Args (o,A)),n)) = ( pi ((((the Sorts of A # ) * the Arity of S) . o),n)) by MSUALG_1:def 4

            .= ( pi (((the Sorts of A # ) . (the Arity of S . o)),n)) by FUNCT_2: 15

            .= ( pi (((the Sorts of A # ) . ( the_arity_of o)),n)) by MSUALG_1:def 1

            .= ( pi (( product (the Sorts of A * ( the_arity_of o))),n)) by FINSEQ_2:def 5

            .= ((the Sorts of A * ( the_arity_of o)) . n) by A27, A28, CARD_3: 12

            .= (the Sorts of A . (( the_arity_of o) . n)) by A26, FUNCT_1: 13

            .= (the Sorts of A . (( the_arity_of o) /. n)) by A26, PARTFUN1:def 6;

            then

             A29: (x . n) in (the Sorts of A . (( the_arity_of o) /. n)) by CARD_3:def 6;

            

             A30: n in ( dom (a1 ^ <*x1*>)) or ex k be Nat st k in ( dom b1) & n = (( len (a1 ^ <*x1*>)) + k) by A2, A25, FINSEQ_1: 25;

            now

              per cases by A30, FINSEQ_1: 25;

                suppose

                 A31: n in ( dom a1);

                then

                 A32: (y . n) = (a1 . n) by A4, FINSEQ_1:def 7;

                (x . n) = (a1 . n) by A5, A31, FINSEQ_1:def 7;

                hence thesis by A29, A32, EQREL_1: 5;

              end;

                suppose ex m be Nat st m in ( dom <*x1*>) & n = (( len a1) + m);

                then

                consider m be Nat such that

                 A33: m in ( dom <*x1*>) and

                 A34: n = (( len a1) + m);

                

                 A35: m in ( Seg 1) by A33, FINSEQ_1: 38;

                then

                 A36: m = 1 by FINSEQ_1: 2, TARSKI:def 1;

                then

                 A37: n in ( Seg (( len a1) + 1)) by A34, FINSEQ_1: 4;

                then n in ( Seg (( len a1) + ( len <*y1*>))) by FINSEQ_1: 40;

                then n in ( Seg ( len (a1 ^ <*y1*>))) by FINSEQ_1: 22;

                then n in ( dom (a1 ^ <*y1*>)) by FINSEQ_1:def 3;

                

                then

                 A38: (y . n) = ((a1 ^ <*y1*>) . (( len a1) + 1)) by A3, A34, A36, FINSEQ_1:def 7

                .= y1 by FINSEQ_1: 42;

                n in ( Seg (( len a1) + ( len <*x1*>))) by A37, FINSEQ_1: 40;

                then n in ( Seg ( len (a1 ^ <*x1*>))) by FINSEQ_1: 22;

                then n in ( dom (a1 ^ <*x1*>)) by FINSEQ_1:def 3;

                

                then (x . n) = ((a1 ^ <*x1*>) . (( len a1) + 1)) by A2, A34, A36, FINSEQ_1:def 7

                .= x1 by FINSEQ_1: 42;

                hence thesis by A24, A34, A35, A38, FINSEQ_1: 2, TARSKI:def 1;

              end;

                suppose ex k be Element of NAT st k in ( dom b1) & n = (( len (a1 ^ <*x1*>)) + k);

                then

                consider k be Element of NAT such that

                 A39: k in ( dom b1) and

                 A40: n = (( len (a1 ^ <*x1*>)) + k);

                n = ((( len a1) + ( len <*x1*>)) + k) by A40, FINSEQ_1: 22;

                then n = ((( len a1) + 1) + k) by FINSEQ_1: 40;

                then n = ((( len a1) + ( len <*y1*>)) + k) by FINSEQ_1: 40;

                then n = (( len (a1 ^ <*y1*>)) + k) by FINSEQ_1: 22;

                then

                 A41: (y . n) = (b1 . k) by A3, A39, FINSEQ_1:def 7;

                (x . n) = (b1 . k) by A2, A39, A40, FINSEQ_1:def 7;

                hence thesis by A29, A41, EQREL_1: 5;

              end;

            end;

            hence thesis;

          end;

          then [(( Den (o,A)) . x), (( Den (o,A)) . y)] in (C2 . ( the_result_sort_of o)) by MSUALG_4:def 4;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      hence thesis;

    end;

    theorem :: MSUALG_5:13

    

     Th13: for o be OperSymbol of S holds for C1,C2 be MSCongruence of A holds for C be MSEquivalence-like ManySortedRelation of A st C = (C1 "\/" C2) holds for x1,y1 be object holds for n be Element of NAT holds for a1,a2,b1 be FinSequence st ( len a1) = n & ( len a1) = ( len a2) & for k be Element of NAT st k in ( dom a1) holds [(a1 . k), (a2 . k)] in (C . (( the_arity_of o) /. k)) holds ( [(( Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)), (( Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in (C . ( the_result_sort_of o)) & [x1, y1] in (C . (( the_arity_of o) /. (n + 1))) implies for x be Element of ( Args (o,A)) st x = ((a1 ^ <*x1*>) ^ b1) holds [(( Den (o,A)) . x), (( Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in (C . ( the_result_sort_of o)))

    proof

      let o be OperSymbol of S;

      let C1,C2 be MSCongruence of A;

      let C be MSEquivalence-like ManySortedRelation of A such that

       A1: C = (C1 "\/" C2);

      consider C9 be ManySortedRelation of the Sorts of A such that

       A2: C9 = (C1 (\/) C2) and

       A3: (C1 "\/" C2) = ( EqCl C9) by Def4;

      

       A4: ((C1 . ( the_result_sort_of o)) "\/" (C2 . ( the_result_sort_of o))) = ( EqCl ((C1 . ( the_result_sort_of o)) \/ (C2 . ( the_result_sort_of o)))) by Th1

      .= ( EqCl (C9 . ( the_result_sort_of o))) by A2, PBOOLE:def 4

      .= ((C1 "\/" C2) . ( the_result_sort_of o)) by A3, Def3;

      consider D9 be ManySortedRelation of the Sorts of A such that

       A5: D9 = (C1 (\/) C2) and

       A6: (C1 "\/" C2) = ( EqCl D9) by Def4;

      let x1,y1 be object;

      let n be Element of NAT ;

      let a1,a2,b1 be FinSequence such that

       A7: ( len a1) = n and

       A8: ( len a1) = ( len a2) and

       A9: for k be Element of NAT st k in ( dom a1) holds [(a1 . k), (a2 . k)] in (C . (( the_arity_of o) /. k));

      

       A10: ((C1 . (( the_arity_of o) /. (n + 1))) "\/" (C2 . (( the_arity_of o) /. (n + 1)))) = ( EqCl ((C1 . (( the_arity_of o) /. (n + 1))) \/ (C2 . (( the_arity_of o) /. (n + 1))))) by Th1

      .= ( EqCl (D9 . (( the_arity_of o) /. (n + 1)))) by A5, PBOOLE:def 4

      .= ((C1 "\/" C2) . (( the_arity_of o) /. (n + 1))) by A6, Def3;

      set y = ((a2 ^ <*y1*>) ^ b1);

      assume that

       A11: [(( Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)), (( Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in (C . ( the_result_sort_of o)) and

       A12: [x1, y1] in (C . (( the_arity_of o) /. (n + 1)));

      let x be Element of ( Args (o,A)) such that

       A13: x = ((a1 ^ <*x1*>) ^ b1);

      

       A14: (the Sorts of A . ( the_result_sort_of o)) = (the Sorts of A . (the ResultSort of S . o)) by MSUALG_1:def 2

      .= ((the Sorts of A * the ResultSort of S) . o) by FUNCT_2: 15

      .= ( Result (o,A)) by MSUALG_1:def 5;

      then (( Den (o,A)) . x) in (the Sorts of A . ( the_result_sort_of o));

      then

      consider p be FinSequence such that

       A15: 1 <= ( len p) and

       A16: (( Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)) = (p . 1) and

       A17: (( Den (o,A)) . ((a2 ^ <*x1*>) ^ b1)) = (p . ( len p)) and

       A18: for i be Nat st 1 <= i & i < ( len p) holds [(p . i), (p . (i + 1))] in ((C1 . ( the_result_sort_of o)) \/ (C2 . ( the_result_sort_of o))) by A1, A11, A13, A4, EQREL_1: 28;

      x1 in (the Sorts of A . (( the_arity_of o) /. (n + 1))) by A12, ZFMISC_1: 87;

      then

      consider f be FinSequence such that

       A19: 1 <= ( len f) and

       A20: x1 = (f . 1) and

       A21: y1 = (f . ( len f)) and

       A22: for i be Nat st 1 <= i & i < ( len f) holds [(f . i), (f . (i + 1))] in ((C1 . (( the_arity_of o) /. (n + 1))) \/ (C2 . (( the_arity_of o) /. (n + 1)))) by A1, A12, A10, EQREL_1: 28;

      deffunc G( Nat) = (( Den (o,A)) . ((a2 ^ <*(f . $1)*>) ^ b1));

      consider g be FinSequence such that

       A23: ( len g) = ( len f) & for i be Nat st i in ( dom g) holds (g . i) = G(i) from FINSEQ_1:sch 2;

      

       A24: ( dom g) = ( Seg ( len f)) by A23, FINSEQ_1:def 3;

      

       A25: ( dom x) = ( Seg ( len ((a1 ^ <*x1*>) ^ b1))) by A13, FINSEQ_1:def 3

      .= ( Seg ( len (a1 ^ ( <*x1*> ^ b1)))) by FINSEQ_1: 32

      .= ( Seg (( len a2) + ( len ( <*x1*> ^ b1)))) by A8, FINSEQ_1: 22

      .= ( Seg ( len (a2 ^ ( <*x1*> ^ b1)))) by FINSEQ_1: 22

      .= ( Seg ( len ((a2 ^ <*x1*>) ^ b1))) by FINSEQ_1: 32

      .= ( dom ((a2 ^ <*x1*>) ^ b1)) by FINSEQ_1:def 3;

      ex q be FinSequence st 1 <= ( len q) & (( Den (o,A)) . x) = (q . 1) & (( Den (o,A)) . y) = (q . ( len q)) & for i be Nat st 1 <= i & i < ( len q) holds [(q . i), (q . (i + 1))] in ((C1 . ( the_result_sort_of o)) \/ (C2 . ( the_result_sort_of o)))

      proof

        take q = (p ^ g);

        

         A26: ( len q) = (( len p) + ( len g)) by FINSEQ_1: 22;

        hence 1 <= ( len q) by A15, NAT_1: 12;

        1 in ( dom p) by A15, FINSEQ_3: 25;

        hence (q . 1) = (( Den (o,A)) . x) by A13, A16, FINSEQ_1:def 7;

        

         A27: ( len g) in ( Seg ( len f)) by A19, A23, FINSEQ_1: 1;

        then ( len g) in ( dom g) by A23, FINSEQ_1:def 3;

        

        hence (q . ( len q)) = (g . ( len g)) by A26, FINSEQ_1:def 7

        .= (( Den (o,A)) . y) by A21, A23, A24, A27;

        

         A28: ( len p) <> 0 by A15;

        hereby

          let i be Nat such that

           A29: 1 <= i and

           A30: i < ( len q);

          

           A31: 1 <= i & i < ( len p) or (( len p) + 1) <= i & i < ( len q) or i = ( len p)

          proof

            assume that

             A32: not (1 <= i & i < ( len p)) and

             A33: not ((( len p) + 1) <= i & i < ( len q));

            i <= ( len p) by A30, A33, NAT_1: 13;

            hence thesis by A29, A32, XXREAL_0: 1;

          end;

          

           A34: ( Seg ( len ((a1 ^ <*x1*>) ^ b1))) = ( dom x) by A13, FINSEQ_1:def 3

          .= ( dom ( the_arity_of o)) by MSUALG_3: 6

          .= ( Seg ( len ( the_arity_of o))) by FINSEQ_1:def 3;

          

           A35: ( len ((a2 ^ <*x1*>) ^ b1)) = ( len (a2 ^ ( <*x1*> ^ b1))) by FINSEQ_1: 32

          .= (( len a2) + ( len ( <*x1*> ^ b1))) by FINSEQ_1: 22

          .= ( len (a1 ^ ( <*x1*> ^ b1))) by A8, FINSEQ_1: 22

          .= ( len ((a1 ^ <*x1*>) ^ b1)) by FINSEQ_1: 32

          .= ( len ( the_arity_of o)) by A34, FINSEQ_1: 6;

           A36:

          now

            let k be Element of NAT ;

            assume k in ( dom x);

            then

             A37: k in ( Seg ( len ( the_arity_of o))) by A25, A35, FINSEQ_1:def 3;

            then

             A38: k in ( dom ( the_arity_of o)) by FINSEQ_1:def 3;

            then

             A39: k in ( dom (the Sorts of A * ( the_arity_of o))) by PARTFUN1:def 2;

            reconsider dz = ( dom ( the_arity_of o)) as non empty set by A37, FINSEQ_1:def 3;

            reconsider so = (the Sorts of A * ( the_arity_of o)) as non-empty ManySortedSet of dz;

            

             A40: ( product so) is non empty;

            ( pi (( Args (o,A)),k)) = ( pi ((((the Sorts of A # ) * the Arity of S) . o),k)) by MSUALG_1:def 4

            .= ( pi (((the Sorts of A # ) . (the Arity of S . o)),k)) by FUNCT_2: 15

            .= ( pi (((the Sorts of A # ) . ( the_arity_of o)),k)) by MSUALG_1:def 1

            .= ( pi (( product (the Sorts of A * ( the_arity_of o))),k)) by FINSEQ_2:def 5

            .= ((the Sorts of A * ( the_arity_of o)) . k) by A39, A40, CARD_3: 12

            .= (the Sorts of A . (( the_arity_of o) . k)) by A38, FUNCT_1: 13

            .= (the Sorts of A . (( the_arity_of o) /. k)) by A38, PARTFUN1:def 6;

            hence (x . k) in (the Sorts of A . (( the_arity_of o) /. k)) by CARD_3:def 6;

          end;

          

           A41: ex i1 be Nat st ( len p) = (i1 + 1) by A28, NAT_1: 6;

          now

            per cases by A31;

              suppose

               A42: 1 <= i & i < ( len p);

              then

               A43: (i + 1) <= ( len p) by NAT_1: 13;

              1 <= (i + 1) by A42, NAT_1: 13;

              then (i + 1) in ( dom p) by A43, FINSEQ_3: 25;

              then

               A44: (q . (i + 1)) = (p . (i + 1)) by FINSEQ_1:def 7;

              i in ( dom p) by A42, FINSEQ_3: 25;

              then (q . i) = (p . i) by FINSEQ_1:def 7;

              hence [(q . i), (q . (i + 1))] in ((C1 . ( the_result_sort_of o)) \/ (C2 . ( the_result_sort_of o))) by A18, A42, A44;

            end;

              suppose

               A45: i = ( len p);

              then i in ( Seg ( len p)) by A41, FINSEQ_1: 4;

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

              then

               A46: (q . i) = (( Den (o,A)) . ((a2 ^ <*x1*>) ^ b1)) by A17, A45, FINSEQ_1:def 7;

              

               A47: 1 in ( Seg ( len g)) by A19, A23, FINSEQ_1: 1;

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

              

              then

               A48: (q . (i + 1)) = (g . 1) by A45, FINSEQ_1:def 7

              .= (( Den (o,A)) . ((a2 ^ <*x1*>) ^ b1)) by A20, A23, A24, A47;

              for k be Nat st k in ( dom ((a2 ^ <*x1*>) ^ b1)) holds (((a2 ^ <*x1*>) ^ b1) . k) in (the Sorts of A . (( the_arity_of o) /. k))

              proof

                let k be Nat;

                assume

                 A49: k in ( dom ((a2 ^ <*x1*>) ^ b1));

                then

                 A50: k in ( dom (a2 ^ ( <*x1*> ^ b1))) by FINSEQ_1: 32;

                now

                  per cases by A50, FINSEQ_1: 25;

                    suppose

                     A51: k in ( dom a2);

                    then k in ( Seg ( len a2)) by FINSEQ_1:def 3;

                    then k in ( dom a1) by A8, FINSEQ_1:def 3;

                    then

                     A52: [(a1 . k), (a2 . k)] in (C . (( the_arity_of o) /. k)) by A9;

                    (((a2 ^ <*x1*>) ^ b1) . k) = ((a2 ^ ( <*x1*> ^ b1)) . k) by FINSEQ_1: 32

                    .= (a2 . k) by A51, FINSEQ_1:def 7;

                    hence thesis by A52, ZFMISC_1: 87;

                  end;

                    suppose ex n1 be Nat st n1 in ( dom ( <*x1*> ^ b1)) & k = (( len a2) + n1);

                    then

                    consider n1 be Nat such that

                     A53: n1 in ( dom ( <*x1*> ^ b1)) and

                     A54: k = (( len a2) + n1);

                    (((a2 ^ <*x1*>) ^ b1) . k) = ((a2 ^ ( <*x1*> ^ b1)) . k) by FINSEQ_1: 32

                    .= (( <*x1*> ^ b1) . n1) by A53, A54, FINSEQ_1:def 7

                    .= ((a1 ^ ( <*x1*> ^ b1)) . k) by A8, A53, A54, FINSEQ_1:def 7

                    .= (x . k) by A13, FINSEQ_1: 32;

                    hence thesis by A25, A36, A49;

                  end;

                end;

                hence thesis;

              end;

              then

              reconsider de = ((a2 ^ <*x1*>) ^ b1) as Element of ( Args (o,A)) by A35, MSAFREE2: 5;

              

               A55: ( field (C2 . ( the_result_sort_of o))) = (the Sorts of A . ( the_result_sort_of o)) by EQREL_1: 9;

              ( field (C1 . ( the_result_sort_of o))) = (the Sorts of A . ( the_result_sort_of o)) by EQREL_1: 9;

              

              then ( field ((C1 . ( the_result_sort_of o)) \/ (C2 . ( the_result_sort_of o)))) = ((the Sorts of A . ( the_result_sort_of o)) \/ (the Sorts of A . ( the_result_sort_of o))) by A55, RELAT_1: 18

              .= (the Sorts of A . ( the_result_sort_of o));

              then

               A56: ((C1 . ( the_result_sort_of o)) \/ (C2 . ( the_result_sort_of o))) is_reflexive_in (the Sorts of A . ( the_result_sort_of o)) by RELAT_2:def 9;

              (( Den (o,A)) . de) in (the Sorts of A . ( the_result_sort_of o)) by A14;

              hence [(q . i), (q . (i + 1))] in ((C1 . ( the_result_sort_of o)) \/ (C2 . ( the_result_sort_of o))) by A46, A48, A56, RELAT_2:def 1;

            end;

              suppose

               A57: (( len p) + 1) <= i & i < ( len q);

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

              then

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

              

               A58: 1 <= (j + 1) by NAT_1: 12;

              ( len f) = (( len q) - ( len p)) by A23, A26, XCMPLX_1: 26;

              then

               A59: j < ( len f) by A57, XREAL_1: 9;

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

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

              then

               A60: ((i + 1) - ( len p)) in ( Seg ( len f)) by XCMPLX_1: 29;

              

               A61: 1 <= j by A57, XREAL_1: 19;

              then

               A62: [(f . j), (f . (j + 1))] in ((C1 . (( the_arity_of o) /. (n + 1))) \/ (C2 . (( the_arity_of o) /. (n + 1)))) by A22, A59;

              then

               A63: (f . ((i - ( len p)) + 1)) in (the Sorts of A . (( the_arity_of o) /. (n + 1))) by ZFMISC_1: 87;

              

               A64: for k be Nat st k in ( dom ((a2 ^ <*(f . ((i + 1) - ( len p)))*>) ^ b1)) holds (((a2 ^ <*(f . ((i + 1) - ( len p)))*>) ^ b1) . k) in (the Sorts of A . (( the_arity_of o) /. k))

              proof

                let k be Nat;

                assume

                 A65: k in ( dom ((a2 ^ <*(f . ((i + 1) - ( len p)))*>) ^ b1));

                then

                 A66: k in ( dom (a2 ^ <*(f . ((i + 1) - ( len p)))*>)) or ex n1 be Nat st n1 in ( dom b1) & k = (( len (a2 ^ <*(f . ((i + 1) - ( len p)))*>)) + n1) by FINSEQ_1: 25;

                now

                  per cases by A66, FINSEQ_1: 25;

                    suppose

                     A67: k in ( dom a2);

                    then k in ( Seg ( len a2)) by FINSEQ_1:def 3;

                    then k in ( dom a1) by A8, FINSEQ_1:def 3;

                    then

                     A68: [(a1 . k), (a2 . k)] in (C . (( the_arity_of o) /. k)) by A9;

                    (((a2 ^ <*(f . ((i + 1) - ( len p)))*>) ^ b1) . k) = ((a2 ^ ( <*(f . ((i + 1) - ( len p)))*> ^ b1)) . k) by FINSEQ_1: 32

                    .= (a2 . k) by A67, FINSEQ_1:def 7;

                    hence thesis by A68, ZFMISC_1: 87;

                  end;

                    suppose ex n2 be Nat st n2 in ( dom <*(f . ((i + 1) - ( len p)))*>) & k = (( len a2) + n2);

                    then

                    consider n2 be Nat such that

                     A69: n2 in ( dom <*(f . ((i + 1) - ( len p)))*>) and

                     A70: k = (( len a2) + n2);

                    n2 in ( Seg 1) by A69, FINSEQ_1: 38;

                    then

                     A71: k = (( len a1) + 1) by A8, A70, FINSEQ_1: 2, TARSKI:def 1;

                    then k in ( Seg (( len a2) + 1)) by A8, FINSEQ_1: 4;

                    then k in ( Seg (( len a2) + ( len <*(f . ((i + 1) - ( len p)))*>))) by FINSEQ_1: 40;

                    then k in ( Seg ( len (a2 ^ <*(f . ((i + 1) - ( len p)))*>))) by FINSEQ_1: 22;

                    then k in ( dom (a2 ^ <*(f . ((i + 1) - ( len p)))*>)) by FINSEQ_1:def 3;

                    

                    then (((a2 ^ <*(f . ((i + 1) - ( len p)))*>) ^ b1) . k) = ((a2 ^ <*(f . ((i + 1) - ( len p)))*>) . k) by FINSEQ_1:def 7

                    .= (f . ((i + 1) - ( len p))) by A8, A71, FINSEQ_1: 42;

                    hence thesis by A7, A63, A71, XCMPLX_1: 29;

                  end;

                    suppose

                     A72: ex n1 be Element of NAT st n1 in ( dom b1) & k = (( len (a2 ^ <*(f . ((i + 1) - ( len p)))*>)) + n1);

                    

                     A73: ( len (a1 ^ <*x1*>)) = (( len a1) + ( len <*x1*>)) by FINSEQ_1: 22

                    .= (( len a2) + 1) by A8, FINSEQ_1: 40

                    .= (( len a2) + ( len <*(f . ((i + 1) - ( len p)))*>)) by FINSEQ_1: 40

                    .= ( len (a2 ^ <*(f . ((i + 1) - ( len p)))*>)) by FINSEQ_1: 22;

                    

                     A74: ( dom x) = ( Seg ( len ((a1 ^ <*x1*>) ^ b1))) by A13, FINSEQ_1:def 3

                    .= ( Seg (( len (a1 ^ <*x1*>)) + ( len b1))) by FINSEQ_1: 22

                    .= ( Seg ((( len a1) + ( len <*x1*>)) + ( len b1))) by FINSEQ_1: 22

                    .= ( Seg ((( len a2) + 1) + ( len b1))) by A8, FINSEQ_1: 40

                    .= ( Seg ((( len a2) + ( len <*(f . ((i + 1) - ( len p)))*>)) + ( len b1))) by FINSEQ_1: 40

                    .= ( Seg (( len (a2 ^ <*(f . ((i + 1) - ( len p)))*>)) + ( len b1))) by FINSEQ_1: 22

                    .= ( Seg ( len ((a2 ^ <*(f . ((i + 1) - ( len p)))*>) ^ b1))) by FINSEQ_1: 22

                    .= ( dom ((a2 ^ <*(f . ((i + 1) - ( len p)))*>) ^ b1)) by FINSEQ_1:def 3;

                    consider n1 be Element of NAT such that

                     A75: n1 in ( dom b1) and

                     A76: k = (( len (a2 ^ <*(f . ((i + 1) - ( len p)))*>)) + n1) by A72;

                    (((a2 ^ <*(f . ((i + 1) - ( len p)))*>) ^ b1) . k) = (b1 . n1) by A75, A76, FINSEQ_1:def 7

                    .= (x . k) by A13, A75, A76, A73, FINSEQ_1:def 7;

                    hence thesis by A36, A65, A74;

                  end;

                end;

                hence thesis;

              end;

              

               A77: (f . (i - ( len p))) in (the Sorts of A . (( the_arity_of o) /. (n + 1))) by A62, ZFMISC_1: 87;

              

               A78: for k be Nat st k in ( dom ((a2 ^ <*(f . (i - ( len p)))*>) ^ b1)) holds (((a2 ^ <*(f . (i - ( len p)))*>) ^ b1) . k) in (the Sorts of A . (( the_arity_of o) /. k))

              proof

                let k be Nat;

                assume

                 A79: k in ( dom ((a2 ^ <*(f . (i - ( len p)))*>) ^ b1));

                then

                 A80: k in ( dom (a2 ^ <*(f . (i - ( len p)))*>)) or ex n1 be Nat st n1 in ( dom b1) & k = (( len (a2 ^ <*(f . (i - ( len p)))*>)) + n1) by FINSEQ_1: 25;

                now

                  per cases by A80, FINSEQ_1: 25;

                    suppose

                     A81: k in ( dom a2);

                    then k in ( Seg ( len a2)) by FINSEQ_1:def 3;

                    then k in ( dom a1) by A8, FINSEQ_1:def 3;

                    then

                     A82: [(a1 . k), (a2 . k)] in (C . (( the_arity_of o) /. k)) by A9;

                    (((a2 ^ <*(f . (i - ( len p)))*>) ^ b1) . k) = ((a2 ^ ( <*(f . (i - ( len p)))*> ^ b1)) . k) by FINSEQ_1: 32

                    .= (a2 . k) by A81, FINSEQ_1:def 7;

                    hence thesis by A82, ZFMISC_1: 87;

                  end;

                    suppose ex n2 be Nat st n2 in ( dom <*(f . (i - ( len p)))*>) & k = (( len a2) + n2);

                    then

                    consider n2 be Nat such that

                     A83: n2 in ( dom <*(f . (i - ( len p)))*>) and

                     A84: k = (( len a2) + n2);

                    

                     A85: n2 in ( Seg 1) by A83, FINSEQ_1: 38;

                    then

                     A86: k = (( len a1) + 1) by A8, A84, FINSEQ_1: 2, TARSKI:def 1;

                    then k in ( Seg (( len a2) + 1)) by A8, FINSEQ_1: 4;

                    then k in ( Seg (( len a2) + ( len <*(f . (i - ( len p)))*>))) by FINSEQ_1: 40;

                    then k in ( Seg ( len (a2 ^ <*(f . (i - ( len p)))*>))) by FINSEQ_1: 22;

                    then k in ( dom (a2 ^ <*(f . (i - ( len p)))*>)) by FINSEQ_1:def 3;

                    

                    then (((a2 ^ <*(f . (i - ( len p)))*>) ^ b1) . k) = ((a2 ^ <*(f . (i - ( len p)))*>) . k) by FINSEQ_1:def 7

                    .= (f . (i - ( len p))) by A8, A86, FINSEQ_1: 42;

                    hence thesis by A7, A8, A77, A84, A85, FINSEQ_1: 2, TARSKI:def 1;

                  end;

                    suppose

                     A87: ex n1 be Element of NAT st n1 in ( dom b1) & k = (( len (a2 ^ <*(f . (i - ( len p)))*>)) + n1);

                    

                     A88: ( len (a1 ^ <*x1*>)) = (( len a1) + ( len <*x1*>)) by FINSEQ_1: 22

                    .= (( len a2) + 1) by A8, FINSEQ_1: 40

                    .= (( len a2) + ( len <*(f . (i - ( len p)))*>)) by FINSEQ_1: 40

                    .= ( len (a2 ^ <*(f . (i - ( len p)))*>)) by FINSEQ_1: 22;

                    

                     A89: ( dom x) = ( Seg ( len ((a1 ^ <*x1*>) ^ b1))) by A13, FINSEQ_1:def 3

                    .= ( Seg (( len (a1 ^ <*x1*>)) + ( len b1))) by FINSEQ_1: 22

                    .= ( Seg ((( len a1) + ( len <*x1*>)) + ( len b1))) by FINSEQ_1: 22

                    .= ( Seg ((( len a2) + 1) + ( len b1))) by A8, FINSEQ_1: 40

                    .= ( Seg ((( len a2) + ( len <*(f . (i - ( len p)))*>)) + ( len b1))) by FINSEQ_1: 40

                    .= ( Seg (( len (a2 ^ <*(f . (i - ( len p)))*>)) + ( len b1))) by FINSEQ_1: 22

                    .= ( Seg ( len ((a2 ^ <*(f . (i - ( len p)))*>) ^ b1))) by FINSEQ_1: 22

                    .= ( dom ((a2 ^ <*(f . (i - ( len p)))*>) ^ b1)) by FINSEQ_1:def 3;

                    consider n1 be Element of NAT such that

                     A90: n1 in ( dom b1) and

                     A91: k = (( len (a2 ^ <*(f . (i - ( len p)))*>)) + n1) by A87;

                    (((a2 ^ <*(f . (i - ( len p)))*>) ^ b1) . k) = (b1 . n1) by A90, A91, FINSEQ_1:def 7

                    .= (x . k) by A13, A90, A91, A88, FINSEQ_1:def 7;

                    hence thesis by A36, A79, A89;

                  end;

                end;

                hence thesis;

              end;

              

               A92: 1 <= j by A57, XREAL_1: 19;

              j <= ( len f) by A23, A26, A57, XREAL_1: 19;

              then

               A93: (i - ( len p)) in ( Seg ( len f)) by A92, FINSEQ_1: 1;

              

               A94: ( Seg ( len ((a1 ^ <*x1*>) ^ b1))) = ( dom x) by A13, FINSEQ_1:def 3

              .= ( dom ( the_arity_of o)) by MSUALG_3: 6

              .= ( Seg ( len ( the_arity_of o))) by FINSEQ_1:def 3;

              

               A95: ( len ((a2 ^ <*(f . ((i + 1) - ( len p)))*>) ^ b1)) = (( len (a2 ^ <*(f . ((i + 1) - ( len p)))*>)) + ( len b1)) by FINSEQ_1: 22

              .= ((( len a2) + ( len <*(f . ((i + 1) - ( len p)))*>)) + ( len b1)) by FINSEQ_1: 22

              .= ((( len a2) + 1) + ( len b1)) by FINSEQ_1: 40

              .= ((( len a1) + ( len <*x1*>)) + ( len b1)) by A8, FINSEQ_1: 40

              .= (( len (a1 ^ <*x1*>)) + ( len b1)) by FINSEQ_1: 22

              .= ( len ((a1 ^ <*x1*>) ^ b1)) by FINSEQ_1: 22

              .= ( len ( the_arity_of o)) by A94, FINSEQ_1: 6;

              ( len ((a2 ^ <*(f . (i - ( len p)))*>) ^ b1)) = (( len (a2 ^ <*(f . (i - ( len p)))*>)) + ( len b1)) by FINSEQ_1: 22

              .= ((( len a2) + ( len <*(f . (i - ( len p)))*>)) + ( len b1)) by FINSEQ_1: 22

              .= ((( len a2) + 1) + ( len b1)) by FINSEQ_1: 40

              .= ((( len a1) + ( len <*x1*>)) + ( len b1)) by A8, FINSEQ_1: 40

              .= (( len (a1 ^ <*x1*>)) + ( len b1)) by FINSEQ_1: 22

              .= ( len ((a1 ^ <*x1*>) ^ b1)) by FINSEQ_1: 22

              .= ( len ( the_arity_of o)) by A94, FINSEQ_1: 6;

              then

              reconsider d1 = ((a2 ^ <*(f . (i - ( len p)))*>) ^ b1), d2 = ((a2 ^ <*(f . ((i + 1) - ( len p)))*>) ^ b1) as Element of ( Args (o,A)) by A78, A64, A95, MSAFREE2: 5;

              

               A96: (q . i) = (g . (i - ( len p))) by A26, A57, FINSEQ_1: 23

              .= (( Den (o,A)) . d1) by A23, A24, A93;

              ((i + 1) - ( len p)) = ((i - ( len p)) + 1) by XCMPLX_1: 29;

              then

               A97: [(f . (i - ( len p))), (f . ((i + 1) - ( len p)))] in ((C1 . (( the_arity_of o) /. (n + 1))) \/ (C2 . (( the_arity_of o) /. (n + 1)))) by A22, A61, A59;

              

               A98: (i + 1) <= ( len q) by A57, NAT_1: 13;

              (( len p) + 1) <= (i + 1) by A57, NAT_1: 12;

              

              then (q . (i + 1)) = (g . ((i + 1) - ( len p))) by A26, A98, FINSEQ_1: 23

              .= (( Den (o,A)) . d2) by A23, A24, A60;

              hence [(q . i), (q . (i + 1))] in ((C1 . ( the_result_sort_of o)) \/ (C2 . ( the_result_sort_of o))) by A7, A8, A96, A97, Th12;

            end;

          end;

          hence [(q . i), (q . (i + 1))] in ((C1 . ( the_result_sort_of o)) \/ (C2 . ( the_result_sort_of o)));

        end;

      end;

      hence thesis by A1, A4, A14, EQREL_1: 28;

    end;

    theorem :: MSUALG_5:14

    

     Th14: for o be OperSymbol of S holds for C1,C2 be MSCongruence of A holds for C be MSEquivalence-like ManySortedRelation of A st C = (C1 "\/" C2) holds for x,y be Element of ( Args (o,A)) holds ((for n be Nat st n in ( dom x) holds [(x . n), (y . n)] in (C . (( the_arity_of o) /. n))) implies [(( Den (o,A)) . x), (( Den (o,A)) . y)] in (C . ( the_result_sort_of o)))

    proof

      set b1 = {} ;

      let o be OperSymbol of S;

      let C1,C2 be MSCongruence of A;

      let C be MSEquivalence-like ManySortedRelation of A such that

       A1: C = (C1 "\/" C2);

      let x,y be Element of ( Args (o,A));

      defpred P[ Nat] means for a1,a2,b1 be FinSequence holds ((( len a1) = $1 & ( len a1) = ( len a2) & x = (a1 ^ b1) & for n be Nat st n in ( dom a1) holds [(x . n), ((a2 ^ b1) . n)] in (C . (( the_arity_of o) /. n))) implies [(( Den (o,A)) . x), (( Den (o,A)) . (a2 ^ b1))] in (C . ( the_result_sort_of o)));

      

       A2: for l be Nat st P[l] holds P[(l + 1)]

      proof

        let l be Nat such that

         A3: for a1,a2,b1 be FinSequence holds ((( len a1) = l & ( len a1) = ( len a2) & x = (a1 ^ b1) & for n be Nat st n in ( dom a1) holds [(x . n), ((a2 ^ b1) . n)] in (C . (( the_arity_of o) /. n))) implies [(( Den (o,A)) . x), (( Den (o,A)) . (a2 ^ b1))] in (C . ( the_result_sort_of o)));

        let a1,a2,b1 be FinSequence;

        assume that

         A4: ( len a1) = (l + 1) and

         A5: ( len a1) = ( len a2) and

         A6: x = (a1 ^ b1) and

         A7: for n be Nat st n in ( dom a1) holds [(x . n), ((a2 ^ b1) . n)] in (C . (( the_arity_of o) /. n));

        

         A8: (l + 1) in ( Seg ( len a1)) by A4, FINSEQ_1: 4;

        then

         A9: (l + 1) in ( dom a2) by A5, FINSEQ_1:def 3;

        set y = (a2 ^ b1);

        a2 <> {} by A4, A5;

        then

        consider q2 be FinSequence, y1 be object such that

         A10: a2 = (q2 ^ <*y1*>) by FINSEQ_1: 46;

        

         A11: (l + 1) = (( len q2) + ( len <*y1*>)) by A4, A5, A10, FINSEQ_1: 22

        .= (( len q2) + 1) by FINSEQ_1: 40;

        

        then

         A12: y1 = (a2 . (l + 1)) by A10, FINSEQ_1: 42

        .= (y . (l + 1)) by A9, FINSEQ_1:def 7;

        a1 <> {} by A4;

        then

        consider q1 be FinSequence, x1 be object such that

         A13: a1 = (q1 ^ <*x1*>) by FINSEQ_1: 46;

        

         A14: (l + 1) = (( len q1) + ( len <*x1*>)) by A4, A13, FINSEQ_1: 22

        .= (( len q1) + 1) by FINSEQ_1: 40;

        then

         A15: ( len q1) = ( len q2) by A11, XCMPLX_1: 2;

        

         A16: ( dom q1) = ( Seg ( len q1)) by FINSEQ_1:def 3

        .= ( dom q2) by A15, FINSEQ_1:def 3;

        

         A17: for n be Element of NAT st n in ( dom q1) holds [(q1 . n), (q2 . n)] in (C . (( the_arity_of o) /. n))

        proof

          let n be Element of NAT ;

          ( len q1) <= ( len a1) by A4, A14, NAT_1: 11;

          then

           A18: ( Seg ( len q1)) c= ( Seg ( len a1)) by FINSEQ_1: 5;

          assume

           A19: n in ( dom q1);

          then n in ( Seg ( len q1)) by FINSEQ_1:def 3;

          then n in ( Seg ( len a1)) by A18;

          then

           A20: n in ( dom a1) by FINSEQ_1:def 3;

          

          then

           A21: (x . n) = (a1 . n) by A6, FINSEQ_1:def 7

          .= (q1 . n) by A13, A19, FINSEQ_1:def 7;

          ( dom a1) = ( Seg ( len a1)) by FINSEQ_1:def 3

          .= ( dom a2) by A5, FINSEQ_1:def 3;

          

          then (y . n) = (a2 . n) by A20, FINSEQ_1:def 7

          .= (q2 . n) by A10, A16, A19, FINSEQ_1:def 7;

          hence thesis by A7, A20, A21;

        end;

        

         A22: (l + 1) in ( dom a1) by A8, FINSEQ_1:def 3;

        

         A23: ((q1 ^ <*x1*>) ^ b1) = (q1 ^ ( <*x1*> ^ b1)) by FINSEQ_1: 32;

        

         A24: ((q2 ^ <*x1*>) ^ b1) = (q2 ^ ( <*x1*> ^ b1)) by FINSEQ_1: 32;

        

         A25: for n be Nat st n in ( dom q1) holds [(x . n), (((q2 ^ <*x1*>) ^ b1) . n)] in (C . (( the_arity_of o) /. n))

        proof

          let n be Nat;

          assume

           A26: n in ( dom q1);

          then

           A27: (((q2 ^ <*x1*>) ^ b1) . n) = (q2 . n) by A16, A24, FINSEQ_1:def 7;

          (x . n) = (q1 . n) by A6, A13, A23, A26, FINSEQ_1:def 7;

          hence thesis by A17, A26, A27;

        end;

        x1 = (a1 . (l + 1)) by A13, A14, FINSEQ_1: 42

        .= (x . (l + 1)) by A6, A22, FINSEQ_1:def 7;

        then

         A28: [x1, y1] in (C . (( the_arity_of o) /. (l + 1))) by A7, A22, A12;

        ( len q1) = l by A14, XCMPLX_1: 2;

        then [(( Den (o,A)) . x), (( Den (o,A)) . ((q2 ^ <*x1*>) ^ b1))] in (C . ( the_result_sort_of o)) by A3, A6, A13, A15, A23, A24, A25;

        hence thesis by A1, A6, A13, A10, A14, A15, A17, A28, Th13;

      end;

      

       A29: ( dom y) = ( dom ( the_arity_of o)) by MSUALG_3: 6

      .= ( Seg ( len ( the_arity_of o))) by FINSEQ_1:def 3;

      ( dom x) = ( dom ( the_arity_of o)) by MSUALG_3: 6

      .= ( Seg ( len ( the_arity_of o))) by FINSEQ_1:def 3;

      then

      reconsider a1 = x, a2 = y as FinSequence by A29, FINSEQ_1:def 2;

      assume

       A30: for n be Nat st n in ( dom x) holds [(x . n), (y . n)] in (C . (( the_arity_of o) /. n));

      

       A31: ( Seg ( len a2)) = ( dom a2) by FINSEQ_1:def 3

      .= ( dom ( the_arity_of o)) by MSUALG_3: 6

      .= ( Seg ( len ( the_arity_of o))) by FINSEQ_1:def 3;

      ( Seg ( len a1)) = ( dom a1) by FINSEQ_1:def 3

      .= ( dom ( the_arity_of o)) by MSUALG_3: 6

      .= ( Seg ( len ( the_arity_of o))) by FINSEQ_1:def 3;

      then

       A32: ( len a1) = ( len a2) by A31, FINSEQ_1: 6;

      

       A33: x = (a1 ^ b1) by FINSEQ_1: 34;

      

       A34: y = (a2 ^ b1) by FINSEQ_1: 34;

      

       A35: P[ 0 ]

      proof

        ( field (C . ( the_result_sort_of o))) = (the Sorts of A . ( the_result_sort_of o)) by ORDERS_1: 12;

        then

         A36: (C . ( the_result_sort_of o)) is_reflexive_in (the Sorts of A . ( the_result_sort_of o)) by RELAT_2:def 9;

        

         A37: (the Sorts of A . ( the_result_sort_of o)) = (the Sorts of A . (the ResultSort of S . o)) by MSUALG_1:def 2

        .= ((the Sorts of A * the ResultSort of S) . o) by FUNCT_2: 15

        .= ( Result (o,A)) by MSUALG_1:def 5;

        let a1,a2,b1 be FinSequence;

        assume that

         A38: ( len a1) = 0 and

         A39: ( len a1) = ( len a2) and

         A40: x = (a1 ^ b1) and for n be Nat st n in ( dom a1) holds [(x . n), ((a2 ^ b1) . n)] in (C . (( the_arity_of o) /. n));

        

         A41: a1 = {} by A38;

        a2 = {} by A38, A39;

        hence thesis by A40, A41, A37, A36, RELAT_2:def 1;

      end;

      for l be Nat holds P[l] from NAT_1:sch 2( A35, A2);

      hence thesis by A30, A32, A33, A34;

    end;

    theorem :: MSUALG_5:15

    

     Th15: for C1,C2 be MSCongruence of A holds (C1 "\/" C2) is MSCongruence of A

    proof

      let C1,C2 be MSCongruence of A;

      reconsider C = (C1 "\/" C2) as MSEquivalence_Relation-like ManySortedRelation of the Sorts of A;

      reconsider C as ManySortedRelation of A;

      reconsider C as MSEquivalence-like ManySortedRelation of A by MSUALG_4:def 3;

      for o be OperSymbol of S, x,y be Element of ( Args (o,A)) st (for n be Nat st n in ( dom x) holds [(x . n), (y . n)] in (C . (( the_arity_of o) /. n))) holds [(( Den (o,A)) . x), (( Den (o,A)) . y)] in (C . ( the_result_sort_of o)) by Th14;

      hence thesis by MSUALG_4:def 4;

    end;

    theorem :: MSUALG_5:16

    

     Th16: for C1,C2 be MSCongruence of A holds (C1 (/\) C2) is MSCongruence of A

    proof

      let C1,C2 be MSCongruence of A;

      reconsider C = (C1 (/\) C2) as Equivalence_Relation of the Sorts of A by Th11;

      reconsider C as MSEquivalence_Relation-like ManySortedRelation of the Sorts of A;

      reconsider C as ManySortedRelation of A;

      reconsider C as MSEquivalence-like ManySortedRelation of A by MSUALG_4:def 3;

      for o be OperSymbol of S, x,y be Element of ( Args (o,A)) st (for n be Nat st n in ( dom x) holds [(x . n), (y . n)] in (C . (( the_arity_of o) /. n))) holds [(( Den (o,A)) . x), (( Den (o,A)) . y)] in (C . ( the_result_sort_of o))

      proof

        let o be OperSymbol of S;

        let x,y be Element of ( Args (o,A)) such that

         A1: for n be Nat st n in ( dom x) holds [(x . n), (y . n)] in (C . (( the_arity_of o) /. n));

        for n be Nat st n in ( dom x) holds [(x . n), (y . n)] in (C1 . (( the_arity_of o) /. n))

        proof

          let n be Nat;

          assume n in ( dom x);

          then [(x . n), (y . n)] in (C . (( the_arity_of o) /. n)) by A1;

          then [(x . n), (y . n)] in ((C1 . (( the_arity_of o) /. n)) /\ (C2 . (( the_arity_of o) /. n))) by PBOOLE:def 5;

          hence thesis by XBOOLE_0:def 4;

        end;

        then

         A2: [(( Den (o,A)) . x), (( Den (o,A)) . y)] in (C1 . ( the_result_sort_of o)) by MSUALG_4:def 4;

        for n be Nat st n in ( dom x) holds [(x . n), (y . n)] in (C2 . (( the_arity_of o) /. n))

        proof

          let n be Nat;

          assume n in ( dom x);

          then [(x . n), (y . n)] in (C . (( the_arity_of o) /. n)) by A1;

          then [(x . n), (y . n)] in ((C1 . (( the_arity_of o) /. n)) /\ (C2 . (( the_arity_of o) /. n))) by PBOOLE:def 5;

          hence thesis by XBOOLE_0:def 4;

        end;

        then

         A3: [(( Den (o,A)) . x), (( Den (o,A)) . y)] in (C2 . ( the_result_sort_of o)) by MSUALG_4:def 4;

        ((C1 . ( the_result_sort_of o)) /\ (C2 . ( the_result_sort_of o))) = (C . ( the_result_sort_of o)) by PBOOLE:def 5;

        hence thesis by A2, A3, XBOOLE_0:def 4;

      end;

      hence thesis by MSUALG_4:def 4;

    end;

    definition

      let S;

      let A be non-empty MSAlgebra over S;

      :: MSUALG_5:def6

      func CongrLatt A -> strict SubLattice of ( EqRelLatt the Sorts of A) means

      : Def6: for x be set holds x in the carrier of it iff x is MSCongruence of A;

      existence

      proof

        set D = the carrier of ( EqRelLatt the Sorts of A);

        set f = the MSCongruence of A;

        defpred P[ object] means $1 is MSCongruence of A;

        deffunc F( Element of S) = ( bool [:(the Sorts of A . $1), (the Sorts of A . $1):]);

        consider M2 be ManySortedSet of the carrier of S such that

         A1: for i be Element of the carrier of S holds (M2 . i) = F(i) from PBOOLE:sch 5;

        consider B be set such that

         A2: for x be object holds x in B iff x in ( product M2) & P[x] from XBOOLE_0:sch 1;

        

         A3: for C1 be MSCongruence of A holds C1 in ( product M2)

        proof

          let C1 be MSCongruence of A;

           A4:

          now

            let x be object;

            assume x in ( dom M2);

            then

            reconsider x9 = x as Element of the carrier of S;

            

             A5: (C1 . x9) is Subset of [:(the Sorts of A . x9), (the Sorts of A . x9):];

            (M2 . x9) = ( bool [:(the Sorts of A . x9), (the Sorts of A . x9):]) by A1;

            hence (C1 . x) in (M2 . x) by A5;

          end;

          ( dom C1) = the carrier of S by PARTFUN1:def 2

          .= ( dom M2) by PARTFUN1:def 2;

          hence thesis by A4, CARD_3: 9;

        end;

        

         A6: for x be set holds x in B iff x is MSCongruence of A by A2, A3;

        then f in B;

        then

        reconsider B as non empty set;

        set B1 = (the L_join of ( EqRelLatt the Sorts of A) || B);

        set B2 = (the L_meet of ( EqRelLatt the Sorts of A) || B);

        now

          let x be object;

          assume x in B;

          then x is MSCongruence of A by A6;

          hence x in the carrier of ( EqRelLatt the Sorts of A) by Def5;

        end;

        then

         A7: B c= D by TARSKI:def 3;

        then [:B, B:] c= [:D, D:] by ZFMISC_1: 96;

        then

        reconsider B1, B2 as Function of [:B, B:], D by FUNCT_2: 32;

        

         A8: ( dom B2) = [:B, B:] by FUNCT_2:def 1;

        now

          let x be object;

          assume

           A9: x in [:B, B:];

          then

          consider x1,x2 be object such that

           A10: x = [x1, x2] by RELAT_1:def 1;

          

           A11: x2 in B by A9, A10, ZFMISC_1: 87;

          x1 in B by A9, A10, ZFMISC_1: 87;

          then

          reconsider x19 = x1, x29 = x2 as MSCongruence of A by A6, A11;

          

           A12: x29 in B by A6;

          x19 in B by A6;

          then [x1, x2] in [:B, B:] by A12, ZFMISC_1: 87;

          

          then (B2 . x) = (the L_meet of ( EqRelLatt the Sorts of A) . (x1,x2)) by A10, FUNCT_1: 49

          .= (x19 (/\) x29) by Def5;

          then (B2 . x) is MSCongruence of A by Th16;

          hence (B2 . x) in B by A6;

        end;

        then

        reconsider B2 as BinOp of B by A8, FUNCT_2: 3;

        

         A13: ( dom B1) = [:B, B:] by FUNCT_2:def 1;

        now

          let x be object;

          assume

           A14: x in [:B, B:];

          then

          consider x1,x2 be object such that

           A15: x = [x1, x2] by RELAT_1:def 1;

          

           A16: x2 in B by A14, A15, ZFMISC_1: 87;

          x1 in B by A14, A15, ZFMISC_1: 87;

          then

          reconsider x19 = x1, x29 = x2 as MSCongruence of A by A6, A16;

          

           A17: x29 in B by A6;

          x19 in B by A6;

          then [x1, x2] in [:B, B:] by A17, ZFMISC_1: 87;

          

          then (B1 . x) = (the L_join of ( EqRelLatt the Sorts of A) . (x1,x2)) by A15, FUNCT_1: 49

          .= (x19 "\/" x29) by Def5;

          then (B1 . x) is MSCongruence of A by Th15;

          hence (B1 . x) in B by A6;

        end;

        then

        reconsider B1 as BinOp of B by A13, FUNCT_2: 3;

        reconsider L = LattStr (# B, B1, B2 #) as non empty LattStr;

        

         A18: for a,b be MSCongruence of A holds (B1 . (a,b)) = (a "\/" b) & (B2 . (a,b)) = (a (/\) b)

        proof

          let a,b be MSCongruence of A;

          

           A19: b in B by A6;

          a in B by A6;

          then

           A20: [a, b] in [:B, B:] by A19, ZFMISC_1: 87;

          

          hence (B1 . (a,b)) = (the L_join of ( EqRelLatt the Sorts of A) . (a,b)) by FUNCT_1: 49

          .= (a "\/" b) by Def5;

          

          thus (B2 . (a,b)) = (the L_meet of ( EqRelLatt the Sorts of A) . (a,b)) by A20, FUNCT_1: 49

          .= (a (/\) b) by Def5;

        end;

         A21:

        now

          let a,b be Element of B;

          reconsider a9 = a, b9 = b as MSCongruence of A by A6;

          

          thus (B1 . (a,b)) = (a9 "\/" b9) by A18

          .= (B1 . (b,a)) by A18;

        end;

        

         A22: for a,b be Element of L holds (a "\/" b) = (b "\/" a)

        proof

          let a,b be Element of L;

          

          thus (a "\/" b) = (B1 . (a,b)) by LATTICES:def 1

          .= (the L_join of L . (b,a)) by A21

          .= (b "\/" a) by LATTICES:def 1;

        end;

         A23:

        now

          let a,b,c be Element of B;

          reconsider a9 = a, b9 = b, c9 = c as MSCongruence of A by A6;

          reconsider e1 = (b9 (/\) c9) as MSCongruence of A by Th16;

          reconsider e2 = (a9 (/\) b9) as MSCongruence of A by Th16;

          

          thus (B2 . (a,(B2 . (b,c)))) = (B2 . (a,e1)) by A18

          .= (a9 (/\) (b9 (/\) c9)) by A18

          .= ((a9 (/\) b9) (/\) c9) by PBOOLE: 29

          .= (B2 . (e2,c)) by A18

          .= (B2 . ((B2 . (a,b)),c)) by A18;

        end;

        

         A24: for a,b,c be Element of L holds (a "/\" (b "/\" c)) = ((a "/\" b) "/\" c)

        proof

          let a,b,c be Element of L;

          

          thus (a "/\" (b "/\" c)) = (the L_meet of L . (a,(b "/\" c))) by LATTICES:def 2

          .= (B2 . (a,(B2 . (b,c)))) by LATTICES:def 2

          .= (the L_meet of L . ((the L_meet of L . (a,b)),c)) by A23

          .= (the L_meet of L . ((a "/\" b),c)) by LATTICES:def 2

          .= ((a "/\" b) "/\" c) by LATTICES:def 2;

        end;

         A25:

        now

          let a,b,c be Element of B;

          reconsider a9 = a, b9 = b, c9 = c as MSCongruence of A by A6;

          reconsider d = (b9 "\/" c9) as MSCongruence of A by Th15;

          reconsider e = (a9 "\/" b9) as MSCongruence of A by Th15;

          

          thus (B1 . (a,(B1 . (b,c)))) = (B1 . (a,d)) by A18

          .= (a9 "\/" (b9 "\/" c9)) by A18

          .= ((a9 "\/" b9) "\/" c9) by Th8

          .= (B1 . (e,c)) by A18

          .= (B1 . ((B1 . (a,b)),c)) by A18;

        end;

        

         A26: for a,b,c be Element of L holds (a "\/" (b "\/" c)) = ((a "\/" b) "\/" c)

        proof

          let a,b,c be Element of L;

          

          thus (a "\/" (b "\/" c)) = (the L_join of L . (a,(b "\/" c))) by LATTICES:def 1

          .= (B1 . (a,(B1 . (b,c)))) by LATTICES:def 1

          .= (the L_join of L . ((the L_join of L . (a,b)),c)) by A25

          .= (the L_join of L . ((a "\/" b),c)) by LATTICES:def 1

          .= ((a "\/" b) "\/" c) by LATTICES:def 1;

        end;

         A27:

        now

          let a,b be Element of B;

          reconsider a9 = a, b9 = b as MSCongruence of A by A6;

          

          thus (B2 . (a,b)) = (b9 (/\) a9) by A18

          .= (B2 . (b,a)) by A18;

        end;

        

         A28: for a,b be Element of L holds (a "/\" b) = (b "/\" a)

        proof

          let a,b be Element of L;

          

          thus (a "/\" b) = (B2 . (a,b)) by LATTICES:def 2

          .= (the L_meet of L . (b,a)) by A27

          .= (b "/\" a) by LATTICES:def 2;

        end;

        

         A29: for a,b be Element of L holds (a "/\" (a "\/" b)) = a

        proof

          let a,b be Element of L;

          

           A30: (B2 . (a,(B1 . (a,b)))) = a

          proof

            reconsider a9 = a, b9 = b as MSCongruence of A by A6;

            reconsider d = (a9 "\/" b9) as MSCongruence of A by Th15;

            

            thus (B2 . (a,(B1 . (a,b)))) = (B2 . (a,d)) by A18

            .= (a9 (/\) (a9 "\/" b9)) by A18

            .= a by Th9;

          end;

          

          thus (a "/\" (a "\/" b)) = (the L_meet of L . (a,(a "\/" b))) by LATTICES:def 2

          .= a by A30, LATTICES:def 1;

        end;

        for a,b be Element of L holds ((a "/\" b) "\/" b) = b

        proof

          let a,b be Element of L;

          

           A31: (B1 . ((B2 . (a,b)),b)) = b

          proof

            reconsider a9 = a, b9 = b as MSCongruence of A by A6;

            reconsider EQR = (a9 (/\) b9) as MSCongruence of A by Th16;

            

            thus (B1 . ((B2 . (a,b)),b)) = (B1 . ((a9 (/\) b9),b9)) by A18

            .= (EQR "\/" b9) by A18

            .= b by Th10;

          end;

          

          thus ((a "/\" b) "\/" b) = (the L_join of L . ((a "/\" b),b)) by LATTICES:def 1

          .= b by A31, LATTICES:def 2;

        end;

        then L is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing by A22, A26, A28, A24, A29, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;

        then

        reconsider L as Lattice;

        reconsider L as strict SubLattice of ( EqRelLatt the Sorts of A) by A7, NAT_LAT:def 12;

        take L;

        thus thesis by A6;

      end;

      uniqueness

      proof

        let C1,C2 be strict SubLattice of ( EqRelLatt the Sorts of A) such that

         A32: for x be set holds x in the carrier of C1 iff x is MSCongruence of A and

         A33: for x be set holds x in the carrier of C2 iff x is MSCongruence of A;

         A34:

        now

          let x be object;

          x in the carrier of C2 iff x is MSCongruence of A by A33;

          hence x in the carrier of C1 iff x in the carrier of C2 by A32;

        end;

        then

         A35: the carrier of C1 = the carrier of C2 by TARSKI: 2;

        

        then

         A36: the L_join of C1 = (the L_join of ( EqRelLatt the Sorts of A) || the carrier of C2) by NAT_LAT:def 12

        .= the L_join of C2 by NAT_LAT:def 12;

        the L_meet of C1 = (the L_meet of ( EqRelLatt the Sorts of A) || the carrier of C2) by A35, NAT_LAT:def 12

        .= the L_meet of C2 by NAT_LAT:def 12;

        hence thesis by A34, A36, TARSKI: 2;

      end;

    end

    theorem :: MSUALG_5:17

    

     Th17: ( id the Sorts of A) is MSCongruence of A

    proof

      set J = ( id the Sorts of A);

      for i be set st i in the carrier of S holds (J . i) is Relation of (the Sorts of A . i)

      proof

        let i be set;

        assume i in the carrier of S;

        then (J . i) = ( id (the Sorts of A . i)) by MSUALG_3:def 1;

        hence thesis;

      end;

      then

      reconsider J as ManySortedRelation of the Sorts of A by MSUALG_4:def 1;

      for i be set, R be Relation of (the Sorts of A . i) st i in the carrier of S & (J . i) = R holds R is Equivalence_Relation of (the Sorts of A . i)

      proof

        let i be set;

        let R be Relation of (the Sorts of A . i);

        assume that

         A1: i in the carrier of S and

         A2: (J . i) = R;

        (J . i) = ( id (the Sorts of A . i)) by A1, MSUALG_3:def 1;

        hence thesis by A2;

      end;

      then

      reconsider J as MSEquivalence_Relation-like ManySortedRelation of the Sorts of A by MSUALG_4:def 2;

      reconsider J as ManySortedRelation of A;

      reconsider J as MSEquivalence-like ManySortedRelation of A by MSUALG_4:def 3;

      for o be OperSymbol of S, x,y be Element of ( Args (o,A)) st (for n be Nat st n in ( dom x) holds [(x . n), (y . n)] in (J . (( the_arity_of o) /. n))) holds [(( Den (o,A)) . x), (( Den (o,A)) . y)] in (J . ( the_result_sort_of o))

      proof

        let o be OperSymbol of S;

        let x,y be Element of ( Args (o,A)) such that

         A3: for n be Nat st n in ( dom x) holds [(x . n), (y . n)] in (J . (( the_arity_of o) /. n));

        

         A4: ( dom y) = ( dom ( the_arity_of o)) by MSUALG_3: 6

        .= ( Seg ( len ( the_arity_of o))) by FINSEQ_1:def 3;

        

         A5: ( dom x) = ( dom ( the_arity_of o)) by MSUALG_3: 6

        .= ( Seg ( len ( the_arity_of o))) by FINSEQ_1:def 3;

        then

        reconsider x9 = x, y9 = y as FinSequence by A4, FINSEQ_1:def 2;

        now

          let n be Nat such that

           A6: n in ( dom x);

          (J . (( the_arity_of o) /. n)) = ( id (the Sorts of A . (( the_arity_of o) /. n))) by MSUALG_3:def 1;

          then [(x . n), (y . n)] in ( id (the Sorts of A . (( the_arity_of o) /. n))) by A3, A6;

          hence (x9 . n) = (y9 . n) by RELAT_1:def 10;

        end;

        then

         A7: x = y by A5, A4, FINSEQ_1: 13;

        (( Den (o,A)) . x) in ( Result (o,A));

        then

         A8: (( Den (o,A)) . x) in ((the Sorts of A * the ResultSort of S) . o) by MSUALG_1:def 5;

        o in the carrier' of S;

        then o in ( dom the ResultSort of S) by FUNCT_2:def 1;

        then (( Den (o,A)) . x) in (the Sorts of A . (the ResultSort of S . o)) by A8, FUNCT_1: 13;

        then

         A9: (( Den (o,A)) . x) in (the Sorts of A . ( the_result_sort_of o)) by MSUALG_1:def 2;

        (J . ( the_result_sort_of o)) = ( id (the Sorts of A . ( the_result_sort_of o))) by MSUALG_3:def 1;

        hence thesis by A7, A9, RELAT_1:def 10;

      end;

      hence thesis by MSUALG_4:def 4;

    end;

    theorem :: MSUALG_5:18

    

     Th18: [|the Sorts of A, the Sorts of A|] is MSCongruence of A

    proof

      set J = [|the Sorts of A, the Sorts of A|];

      for i be set st i in the carrier of S holds (J . i) is Relation of (the Sorts of A . i)

      proof

        let i be set;

        assume i in the carrier of S;

        then (J . i) c= [:(the Sorts of A . i), (the Sorts of A . i):] by PBOOLE:def 16;

        hence thesis;

      end;

      then

      reconsider J as ManySortedRelation of the Sorts of A by MSUALG_4:def 1;

      for i be set, R be Relation of (the Sorts of A . i) st i in the carrier of S & (J . i) = R holds R is Equivalence_Relation of (the Sorts of A . i)

      proof

        let i be set;

        let R be Relation of (the Sorts of A . i);

        assume that

         A1: i in the carrier of S and

         A2: (J . i) = R;

        (J . i) = ( nabla (the Sorts of A . i)) by A1, PBOOLE:def 16;

        hence thesis by A2;

      end;

      then

      reconsider J as MSEquivalence_Relation-like ManySortedRelation of the Sorts of A by MSUALG_4:def 2;

      reconsider J as MSEquivalence-like ManySortedRelation of A by MSUALG_4:def 3;

      for o be OperSymbol of S, x,y be Element of ( Args (o,A)) st (for n be Nat st n in ( dom x) holds [(x . n), (y . n)] in (J . (( the_arity_of o) /. n))) holds [(( Den (o,A)) . x), (( Den (o,A)) . y)] in (J . ( the_result_sort_of o))

      proof

        let o be OperSymbol of S;

        let x,y be Element of ( Args (o,A)) such that for n be Nat st n in ( dom x) holds [(x . n), (y . n)] in (J . (( the_arity_of o) /. n));

        o in the carrier' of S;

        then

         A3: o in ( dom the ResultSort of S) by FUNCT_2:def 1;

        (( Den (o,A)) . y) in ( Result (o,A));

        then (( Den (o,A)) . y) in ((the Sorts of A * the ResultSort of S) . o) by MSUALG_1:def 5;

        then (( Den (o,A)) . y) in (the Sorts of A . (the ResultSort of S . o)) by A3, FUNCT_1: 13;

        then

         A4: (( Den (o,A)) . y) in (the Sorts of A . ( the_result_sort_of o)) by MSUALG_1:def 2;

        (( Den (o,A)) . x) in ( Result (o,A));

        then (( Den (o,A)) . x) in ((the Sorts of A * the ResultSort of S) . o) by MSUALG_1:def 5;

        then (( Den (o,A)) . x) in (the Sorts of A . (the ResultSort of S . o)) by A3, FUNCT_1: 13;

        then

         A5: (( Den (o,A)) . x) in (the Sorts of A . ( the_result_sort_of o)) by MSUALG_1:def 2;

        (J . ( the_result_sort_of o)) = [:(the Sorts of A . ( the_result_sort_of o)), (the Sorts of A . ( the_result_sort_of o)):] by PBOOLE:def 16;

        hence thesis by A5, A4, ZFMISC_1: 87;

      end;

      hence thesis by MSUALG_4:def 4;

    end;

    registration

      let S, A;

      cluster ( CongrLatt A) -> bounded;

      coherence

      proof

        ex c be Element of ( CongrLatt A) st for a be Element of ( CongrLatt A) holds (c "\/" a) = c & (a "\/" c) = c

        proof

          reconsider c9 = [|the Sorts of A, the Sorts of A|] as MSCongruence of A by Th18;

          

           A1: the L_join of ( CongrLatt A) = (the L_join of ( EqRelLatt the Sorts of A) || the carrier of ( CongrLatt A)) by NAT_LAT:def 12;

          reconsider c = c9 as Element of ( CongrLatt A) by Def6;

          take c;

          let a be Element of ( CongrLatt A);

          

           A2: [c, a] in [:the carrier of ( CongrLatt A), the carrier of ( CongrLatt A):] by ZFMISC_1: 87;

          reconsider a9 = a as MSCongruence of A by Def6;

           A3:

          now

            let i be object;

            assume

             A4: i in the carrier of S;

            then

            reconsider i9 = i as Element of S;

            

             A5: ex K1 be ManySortedRelation of the Sorts of A st K1 = (c9 (\/) a9) & (c9 "\/" a9) = ( EqCl K1) by Def4;

            reconsider K2 = (c9 . i9), a2 = (a9 . i9) as Equivalence_Relation of (the Sorts of A . i);

            ((c9 (\/) a9) . i) = ((c9 . i) \/ (a9 . i)) by A4, PBOOLE:def 4

            .= (( nabla (the Sorts of A . i)) \/ a2) by PBOOLE:def 16

            .= ( nabla (the Sorts of A . i)) by EQREL_1: 1

            .= (c9 . i) by A4, PBOOLE:def 16;

            

            hence ((c9 "\/" a9) . i) = ( EqCl K2) by A5, Def3

            .= (c9 . i) by Th2;

          end;

          

          thus (c "\/" a) = (the L_join of ( CongrLatt A) . (c,a)) by LATTICES:def 1

          .= (the L_join of ( EqRelLatt the Sorts of A) . (c,a)) by A1, A2, FUNCT_1: 49

          .= (c9 "\/" a9) by Def5

          .= c by A3, PBOOLE: 3;

          hence thesis;

        end;

        then

         A6: ( CongrLatt A) is upper-bounded by LATTICES:def 14;

        ex c be Element of ( CongrLatt A) st for a be Element of ( CongrLatt A) holds (c "/\" a) = c & (a "/\" c) = c

        proof

          reconsider c9 = ( id the Sorts of A) as MSCongruence of A by Th17;

          

           A7: the L_meet of ( CongrLatt A) = (the L_meet of ( EqRelLatt the Sorts of A) || the carrier of ( CongrLatt A)) by NAT_LAT:def 12;

          reconsider c = c9 as Element of ( CongrLatt A) by Def6;

          take c;

          let a be Element of ( CongrLatt A);

          

           A8: [c, a] in [:the carrier of ( CongrLatt A), the carrier of ( CongrLatt A):] by ZFMISC_1: 87;

          reconsider a9 = a as MSCongruence of A by Def6;

           A9:

          now

            let i be object;

            assume

             A10: i in the carrier of S;

            then

            reconsider i9 = i as Element of S;

            reconsider a2 = (a9 . i9) as Equivalence_Relation of (the Sorts of A . i);

            

            thus ((c9 (/\) a9) . i) = ((c9 . i) /\ (a9 . i)) by A10, PBOOLE:def 5

            .= (( id (the Sorts of A . i)) /\ a2) by MSUALG_3:def 1

            .= ( id (the Sorts of A . i)) by EQREL_1: 10

            .= (c9 . i) by A10, MSUALG_3:def 1;

          end;

          

          thus (c "/\" a) = (the L_meet of ( CongrLatt A) . (c,a)) by LATTICES:def 2

          .= (the L_meet of ( EqRelLatt the Sorts of A) . (c,a)) by A7, A8, FUNCT_1: 49

          .= (c9 (/\) a9) by Def5

          .= c by A9, PBOOLE: 3;

          hence thesis;

        end;

        then ( CongrLatt A) is lower-bounded by LATTICES:def 13;

        hence thesis by A6;

      end;

    end

    theorem :: MSUALG_5:19

    ( Bottom ( CongrLatt A)) = ( id the Sorts of A)

    proof

      set K = ( id the Sorts of A);

      K is MSCongruence of A by Th17;

      then

      reconsider K as Element of ( CongrLatt A) by Def6;

      

       A1: the L_meet of ( CongrLatt A) = (the L_meet of ( EqRelLatt the Sorts of A) || the carrier of ( CongrLatt A)) by NAT_LAT:def 12;

      now

        let a be Element of ( CongrLatt A);

        reconsider K9 = K, a9 = a as Equivalence_Relation of the Sorts of A by Def6;

        

         A2: [K, a] in [:the carrier of ( CongrLatt A), the carrier of ( CongrLatt A):] by ZFMISC_1: 87;

         A3:

        now

          let i be object;

          assume

           A4: i in the carrier of S;

          then

          reconsider i9 = i as Element of S;

          reconsider a2 = (a9 . i9) as Equivalence_Relation of (the Sorts of A . i) by MSUALG_4:def 2;

          

          thus ((K9 (/\) a9) . i) = ((K9 . i) /\ (a9 . i)) by A4, PBOOLE:def 5

          .= (( id (the Sorts of A . i)) /\ a2) by MSUALG_3:def 1

          .= ( id (the Sorts of A . i)) by EQREL_1: 10

          .= (K9 . i) by A4, MSUALG_3:def 1;

        end;

        

        thus (K "/\" a) = (the L_meet of ( CongrLatt A) . (K,a)) by LATTICES:def 2

        .= (the L_meet of ( EqRelLatt the Sorts of A) . (K,a)) by A1, A2, FUNCT_1: 49

        .= (K9 (/\) a9) by Def5

        .= K by A3, PBOOLE: 3;

        hence (a "/\" K) = K;

      end;

      hence thesis by LATTICES:def 16;

    end;

    theorem :: MSUALG_5:20

    ( Top ( CongrLatt A)) = [|the Sorts of A, the Sorts of A|]

    proof

      set K = [|the Sorts of A, the Sorts of A|];

      K is MSCongruence of A by Th18;

      then

      reconsider K as Element of ( CongrLatt A) by Def6;

      

       A1: the L_join of ( CongrLatt A) = (the L_join of ( EqRelLatt the Sorts of A) || the carrier of ( CongrLatt A)) by NAT_LAT:def 12;

      now

        let a be Element of ( CongrLatt A);

        reconsider K9 = K, a9 = a as Equivalence_Relation of the Sorts of A by Def6;

        

         A2: [K, a] in [:the carrier of ( CongrLatt A), the carrier of ( CongrLatt A):] by ZFMISC_1: 87;

         A3:

        now

          let i be object;

          assume

           A4: i in the carrier of S;

          then

          reconsider i9 = i as Element of S;

          

           A5: ex K1 be ManySortedRelation of the Sorts of A st K1 = (K9 (\/) a9) & (K9 "\/" a9) = ( EqCl K1) by Def4;

          reconsider K2 = (K9 . i9), a2 = (a9 . i9) as Equivalence_Relation of (the Sorts of A . i) by MSUALG_4:def 2;

          ((K9 (\/) a9) . i) = ((K9 . i) \/ (a9 . i)) by A4, PBOOLE:def 4

          .= (( nabla (the Sorts of A . i)) \/ a2) by PBOOLE:def 16

          .= ( nabla (the Sorts of A . i)) by EQREL_1: 1

          .= (K9 . i) by A4, PBOOLE:def 16;

          

          hence ((K9 "\/" a9) . i) = ( EqCl K2) by A5, Def3

          .= (K9 . i) by Th2;

        end;

        

        thus (K "\/" a) = (the L_join of ( CongrLatt A) . (K,a)) by LATTICES:def 1

        .= (the L_join of ( EqRelLatt the Sorts of A) . (K,a)) by A1, A2, FUNCT_1: 49

        .= (K9 "\/" a9) by Def5

        .= K by A3, PBOOLE: 3;

        hence (a "\/" K) = K;

      end;

      hence thesis by LATTICES:def 17;

    end;

    theorem :: MSUALG_5:21

    for X be set holds x in the carrier of ( EqRelLatt X) iff x is Equivalence_Relation of X

    proof

      let X be set;

      

       A1: the carrier of ( EqRelLatt X) = { x1 where x1 be Relation of X, X : x1 is Equivalence_Relation of X } by Def2;

      thus x in the carrier of ( EqRelLatt X) implies x is Equivalence_Relation of X

      proof

        assume x in the carrier of ( EqRelLatt X);

        then ex x1 be Relation of X, X st x = x1 & x1 is Equivalence_Relation of X by A1;

        hence thesis;

      end;

      thus thesis by A1;

    end;