The Mizar article:

Lattice of Congruences in Many Sorted Algebra

by
Robert Milewski

Received January 11, 1996

Copyright (c) 1996 Association of Mizar Users

MML identifier: MSUALG_5
[ MML identifier index ]


environ

 vocabulary PBOOLE, RELAT_1, EQREL_1, LATTICES, BOOLE, FUNCT_1, BINOP_1,
      MSUALG_4, CARD_3, MSUALG_1, AMI_1, ZF_REFLE, FINSEQ_1, QC_LANG1, TDGROUP,
      RELAT_2, ARYTM_1, NAT_LAT, PRALG_2, MSUALG_5, FINSEQ_4;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XREAL_0, RELAT_1, RELAT_2,
      FUNCT_1, STRUCT_0, PARTFUN1, FUNCT_2, RELSET_1, EQREL_1, BINOP_1, PBOOLE,
      MSUALG_1, MSUALG_3, MSUALG_4, LATTICES, NAT_LAT, CARD_3, PRALG_2,
      FINSEQ_1, FINSEQ_4, REAL_1, NAT_1;
 constructors BINOP_1, MSUALG_3, MSUALG_4, NAT_LAT, REAL_1, NAT_1, FINSEQ_4,
      MEMBERED, EQREL_1;
 clusters SUBSET_1, STRUCT_0, MSUALG_1, LATTICES, NAT_LAT, RELSET_1, MSUALG_4,
      MSUALG_3, PRALG_1, PBOOLE, FINSEQ_1, NAT_1, EQREL_1, PARTFUN1;
 requirements NUMERALS, REAL, BOOLE, SUBSET;
 definitions PBOOLE;
 theorems BINOP_1, PBOOLE, MSUALG_4, EQREL_1, TARSKI, NAT_LAT, LATTICES,
      RELAT_1, RELAT_2, RELSET_1, STRUCT_0, FUNCT_2, CARD_3, ZFMISC_1,
      MSUALG_1, FINSEQ_4, FUNCT_1, MSUALG_3, FINSEQ_1, REAL_1, NAT_1, AXIOMS,
      MSAFREE2, PRALG_2, XBOOLE_0, XBOOLE_1, FINSEQ_3, XCMPLX_1, ORDERS_1;
 schemes MSUALG_1, BINOP_1, NAT_1, FINSEQ_1, PRALG_2, XBOOLE_0;

begin
     :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
     ::                MORE  OF  EQUIVALENCE  RELATIONS               ::
     :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

  reserve I,X,x,y,z,d,i for set;
  reserve M for ManySortedSet of I;
  reserve R1 for Relation of X;
  reserve EqR1,EqR2,EqR3,EqR4 for Equivalence_Relation of X;

  theorem Th1:
   (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3)
  proof
     for EqR4 holds EqR4 = (EqR1 "\/" EqR2) "\/" EqR3 implies
    EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4
   proof
    let EqR4;
    A1: EqR1 "\/" EqR2 c= (EqR1 "\/" EqR2) \/ EqR3 by XBOOLE_1:7;
    A2: EqR3 c= (EqR1 "\/" EqR2) \/ EqR3 by XBOOLE_1:7;
    A3: EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by EQREL_1:def 3;
    A4: EqR1 c= EqR1 \/ EqR2 & EqR2 c= EqR1 \/ EqR2 by XBOOLE_1:7;
    assume EqR4 = (EqR1 "\/" EqR2) "\/" EqR3;
    then A5: (EqR1 "\/" EqR2) \/ EqR3 c= EqR4 by EQREL_1:def 3;
    then EqR1 "\/" EqR2 c= EqR4 by A1,XBOOLE_1:1;
    then EqR1 \/ EqR2 c= EqR4 by A3,XBOOLE_1:1;
    then A6: EqR1 c= EqR4 & EqR2 c= EqR4 & EqR3 c= EqR4 by A2,A4,A5,XBOOLE_1:1;
    then EqR2 \/ EqR3 c= EqR4 by XBOOLE_1:8;
    then EqR2 "\/" EqR3 c= EqR4 by EQREL_1:def 3;
    then EqR1 \/ (EqR2 "\/" EqR3) c= EqR4 by A6,XBOOLE_1:8;
    hence EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4 by EQREL_1:def 3;
   end;
   then A7: EqR1 "\/" (EqR2 "\/" EqR3) c= (EqR1 "\/" EqR2) "\/" EqR3;
     for EqR4 holds EqR4 = EqR1 "\/" (EqR2 "\/" EqR3) implies
    (EqR1 "\/" EqR2) "\/" EqR3 c= EqR4
   proof
    let EqR4;
    A8: EqR2 "\/" EqR3 c= EqR1 \/ (EqR2 "\/" EqR3) by XBOOLE_1:7;
    A9: EqR1 c= EqR1 \/ (EqR2 "\/" EqR3) by XBOOLE_1:7;
    A10: EqR2 \/ EqR3 c= EqR2 "\/" EqR3 by EQREL_1:def 3;
    A11: EqR2 c= EqR2 \/ EqR3 & EqR3 c= EqR2 \/ EqR3 by XBOOLE_1:7;
    assume EqR4 = EqR1 "\/" (EqR2 "\/" EqR3);
    then A12: EqR1 \/ (EqR2 "\/" EqR3) c= EqR4 by EQREL_1:def 3;
    then EqR2 "\/" EqR3 c= EqR4 by A8,XBOOLE_1:1;
    then EqR2 \/ EqR3 c= EqR4 by A10,XBOOLE_1:1;
    then A13: EqR1 c= EqR4 & EqR2 c= EqR4 & EqR3 c= EqR4 by A9,A11,A12,XBOOLE_1
:1
;
    then EqR1 \/ EqR2 c= EqR4 by XBOOLE_1:8;
    then EqR1 "\/" EqR2 c= EqR4 by EQREL_1:def 3;
    then (EqR1 "\/" EqR2) \/ EqR3 c= EqR4 by A13,XBOOLE_1:8;
    hence (EqR1 "\/" EqR2) "\/" EqR3 c= EqR4 by EQREL_1:def 3;
   end;
   then (EqR1 "\/" EqR2) "\/" EqR3 c= EqR1 "\/" (EqR2 "\/" EqR3);
   hence thesis by A7,XBOOLE_0:def 10;
  end;

  definition
   let X be set, R be Relation of X;
   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:20;
   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: C1 c= C2 by A2,A3;
       C2 c= C1 by A1,A4;
     hence C1 = C2 by A5,XBOOLE_0:def 10;
   end;
  end;

  theorem Th2:
   EqR1 "\/" EqR2 = EqCl (EqR1 \/ EqR2)
   proof
      EqR1 \/ EqR2 c= EqR1 "\/" EqR2 & for EqR3 be Equivalence_Relation of X st
    EqR1 \/ EqR2 c= EqR3 holds EqR1 "\/" EqR2 c= EqR3 by EQREL_1:def 3;
    hence thesis by Def1;
   end;

   theorem Th3:
    EqCl EqR1 = EqR1
    proof
       EqR1 c= EqR1 & for EqR2 be Equivalence_Relation of X st EqR1 c= EqR2
      holds EqR1 c= EqR2;
     hence thesis by Def1;
    end;

   theorem Th4:
    nabla X \/ R1 = nabla X
    proof
       now let z;
      assume z in R1;
      then consider x,y such that A1: z = [x,y] & x in X & y in
 X by RELSET_1:6;
        z in [:X,X:] by A1,ZFMISC_1:106;
      hence z in nabla X by EQREL_1:def 1;
     end;
     then R1 c= nabla X by TARSKI:def 3;
     hence thesis by XBOOLE_1:12;
    end;

begin
     :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
     ::               LATTICE  OF  EQUIVALENCE  RELATIONS             ::
     :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

  definition
   let X be set;
   func EqRelLatt X -> strict Lattice means
      the carrier of it = {x where x is Relation of X,X :
                         x is Equivalence_Relation of X} &
    for x,y being 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 is 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 x' be Element of B st $1 \/ $2 c= x' holds
        $3 c= x' );
    A1: for x,y being Element of B ex z being Element of B st Z[x,y,z]
    proof
     let x,y be Element of B;
     A2: x in B & y in B;
     then A3: ex x'' be Relation of X,X st x = x'' &
      x'' is Equivalence_Relation of X;
       ex y'' be Relation of X,X st y = y'' &
      y'' is Equivalence_Relation of X by A2;
     then reconsider x1 = x , y1 = y as Equivalence_Relation of X by A3;
     consider z being Equivalence_Relation of X such that A4: x1 \/ y1 c= z &
      for x' be Equivalence_Relation of X st x1 \/ y1 c= x' holds z c= x'
                                                               by EQREL_1:20;
       z in B;
     then reconsider z' = z as Element of B;
     take z';
     thus x \/ y c= z' by A4;
     hereby let x' be Element of B such that A5: x \/ y c= x';
        x' in B;
      then ex x'' be Relation of X,X st x' = x'' &
       x'' is Equivalence_Relation of X;
      then reconsider x1' = x' as Equivalence_Relation of X;
        x \/ y c= x1' by A5;
      hence z' c= x' by A4;
     end;
    end;
    consider B1 being BinOp of B such that A6:
     for x,y being Element of B holds Z[x,y,B1.(x,y)] from BinOpEx(A1);
    A7: now let x,y be Equivalence_Relation of X;
       x in B & y in B;
     then reconsider x1 = x , y1 = y as Element of B;
     reconsider B1' = B1.(x1,y1) as Element of B;
       B1' in B;
     then ex B1'' be Relation of X,X st B1' = B1'' &
      B1'' is Equivalence_Relation of X;
     then reconsider B1' as Equivalence_Relation of X;
     A8: x1 \/ y1 c= B1.(x1,y1) & for x' be Element of B st
      x1 \/ y1 c= x' holds B1.(x1,y1) c= x' by A6;
       now let x' be Equivalence_Relation of X such that A9: x \/ y c= x';
        x' in B;
      then reconsider x1' = x' as Element of B;
        x \/ y c= x1' by A9;
      hence B1.(x,y) c= x' by A8;
     end;
     then B1' = x "\/" y by A8,EQREL_1:def 3;
     hence B1.(x,y) = x "\/" y;
    end;
    defpred Z[Element of B,Element of B,Element of B] means  $3 = $1 /\ $2;
    A10: for x,y being Element of B ex z being Element of B st Z[x,y,z]
    proof
     let x,y be Element of B;
     A11: x in B & y in B;
     then A12: ex x1 being Relation of X,X st x = x1 &
      x1 is Equivalence_Relation of X;
       ex y1 being Relation of X,X st y = y1 &
      y1 is Equivalence_Relation of X by A11;
     then reconsider x' = x , y' = y as Equivalence_Relation of X by A12;
     set z = x' /\ y';
       z in B;
     then reconsider z as Element of B;
     take z;
     thus z = x /\ y;
    end;
    consider B2 be BinOp of B such that A13:
     for x,y being Element of B holds Z[x,y,B2.(x,y)] from BinOpEx(A10);
    A14: now let x,y be Equivalence_Relation of X;
       x in B & y in B;
     then reconsider x' = x , y' = y as Element of B;
       B2.(x',y') = x' /\ y' by A13;
     hence B2.(x,y) = x /\ y;
    end;
    reconsider L = LattStr (# B,B1,B2 #) as non empty LattStr
      by STRUCT_0:def 1;
    A15: B1 is commutative
    proof
       now let a,b be Element of B;
      A16: a in B & b in B;
      then A17: ex x1 be Relation of X,X st a = x1 &
       x1 is Equivalence_Relation of X;
        ex x2 be Relation of X,X st b = x2 &
       x2 is Equivalence_Relation of X by A16;
      then reconsider U1 = a , U2 = b as Equivalence_Relation of X by A17;
      thus B1.(a,b) = U2 "\/" U1 by A7
                    .= B1.(b,a) by A7;
     end;
     hence thesis by BINOP_1:def 2;
    end;
    A18: B1 is associative
    proof
       now let a,b,c be Element of B;
      A19: a in B & b in B & c in B;
      then A20: ex x1 be Relation of X,X st a = x1 &
       x1 is Equivalence_Relation of X;
      A21: ex x2 be Relation of X,X st b = x2 &
       x2 is Equivalence_Relation of X by A19;
        ex x3 be Relation of X,X st c = x3 &
       x3 is Equivalence_Relation of X by A19;
      then reconsider U1 = a , U2 = b , U3 = c as Equivalence_Relation of X
                                                                    by A20,A21;
      thus B1.(a,B1.(b,c)) = B1.(a,U2 "\/" U3) by A7
                            .= U1 "\/" (U2 "\/" U3) by A7
                            .= (U1 "\/" U2) "\/" U3 by Th1
                            .= B1.(U1 "\/" U2,c) by A7
                            .= B1.(B1.(a,b),c) by A7;
     end;
     hence thesis by BINOP_1:def 3;
    end;
    A22:B2 is commutative
    proof
       now let a,b be Element of B;
      A23: a in B & b in B;
      then A24: ex x1 be Relation of X,X st a = x1 &
       x1 is Equivalence_Relation of X;
        ex x2 be Relation of X,X st b = x2 &
       x2 is Equivalence_Relation of X by A23;
      then reconsider U1 = a , U2 = b as Equivalence_Relation of X by A24;
      thus B2.(a,b) = U2 /\ U1 by A14
                    .= B2.(b,a) by A14;
     end;
     hence thesis by BINOP_1:def 2;
    end;
    A25: B2 is associative
    proof
       now let a,b,c be Element of B;
      A26: a in B & b in B & c in B;
      then A27: ex x1 be Relation of X,X st a = x1 &
       x1 is Equivalence_Relation of X;
      A28: ex x2 be Relation of X,X st b = x2 &
       x2 is Equivalence_Relation of X by A26;
        ex x3 be Relation of X,X st c = x3 &
       x3 is Equivalence_Relation of X by A26;
      then reconsider U1 = a , U2 = b , U3 = c as Equivalence_Relation of X
                                                                    by A27,A28;
      thus B2.(a,B2.(b,c)) = B2.(a,U2 /\ U3) by A14
                            .= U1 /\ (U2 /\ U3) by A14
                            .= (U1 /\ U2) /\ U3 by XBOOLE_1:16
                            .= B2.(U1 /\ U2,c) by A14
                            .= B2.(B2.(a,b),c) by A14;
     end;
     hence thesis by BINOP_1:def 3;
    end;
    A29:for a,b being 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 A15,BINOP_1:def 2
               .=b"\/"a by LATTICES:def 1;
     end;
    A30:for a,b,c being 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;
      A31: (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 A18,BINOP_1:
def 3
               .=(a"\/"b)"\/"c by A31,LATTICES:def 1;
     end;
    A32:for a,b being 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;
      A33:B1.(B2.(x,y),y)= y
       proof
        A34: x in B & y in B;
        then A35: ex x1 be Relation of X,X st x = x1 &
         x1 is Equivalence_Relation of X;
          ex x2 be Relation of X,X st y = x2 &
         x2 is Equivalence_Relation of X by A34;
        then reconsider U1 = x , U2 = y as Equivalence_Relation of X by A35;
          B2.(x,y) = U1 /\ U2 by A14;
        hence B1.(B2.(x,y),y) = (U2 "\/" (U1 /\ U2)) by A7
                             .= y by EQREL_1:25;
       end;
      thus (a"/\"b)"\/"b = (the L_join of L).((a"/\"b),b) by LATTICES:def 1
            .= b by A33,LATTICES:def 2;
     end;
    A36:for a,b being 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 A22,BINOP_1:def 2
               .=b"/\"a by LATTICES:def 2;
     end;
    A37:for a,b,c being 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;
      A38: (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,BINOP_1:
def 3
               .=(a"/\"b)"/\"c by A38,LATTICES:def 2;
     end;
      for a,b being 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;
      A39:B2.(x,B1.(x,y))= x
       proof
        A40: x in B & y in B;
        then A41: ex x1 be Relation of X,X st x = x1 &
         x1 is Equivalence_Relation of X;
          ex x2 be Relation of X,X st y = x2 &
         x2 is Equivalence_Relation of X by A40;
        then reconsider U1= x,U2=y as Equivalence_Relation of X by A41;
          B1.(x,y) = U1 "\/" U2 by A7;
        hence B2.(x,B1.(x,y)) = (U1 /\( U1 "\/" U2)) by A14
                             .= x by EQREL_1:24;
       end;
      thus a"/\"(a"\/"b) = (the L_meet of L).(a,(a"\/"b)) by LATTICES:def 2
            .= a by A39,LATTICES:def 1;
     end;
    then L is join-commutative join-associative meet-absorbing
         meet-commutative meet-associative join-absorbing
     by A29,A30,A32,A36,A37,LATTICES:def 4,def 5,def 6,def 7,def 8,def 9;
    then reconsider L as strict Lattice by LATTICES:def 10;
    take L;
    thus the carrier of L = {x where x is Relation of X,X :
                          x is Equivalence_Relation of X};
    thus for x,y be Equivalence_Relation of X holds
     (the L_meet of L).(x,y) = x /\ y &
     (the L_join of L).(x,y) = x "\/" y by A7,A14;
   end;
   uniqueness
   proof
    let P1,P2 be strict Lattice such that
     A42: the carrier of P1 = {x where x is Relation of X,X :
          x is Equivalence_Relation of X} and
     A43: for x,y being Equivalence_Relation of X holds
          (the L_meet of P1).(x,y) = x /\ y &
          (the L_join of P1).(x,y) = x "\/" y and
     A44: the carrier of P2 = {x where x is Relation of X,X :
          x is Equivalence_Relation of X} and
     A45: for x,y being 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;
     A46: now let x,y be Element of Z;
      A47: x in Z & y in Z;
      then A48: ex x2 be Relation of X,X st x = x2 &
       x2 is Equivalence_Relation of X by A42;
        ex x3 be Relation of X,X st y = x3 &
       x3 is Equivalence_Relation of X by A42,A47;
      then reconsider x1 = x , y1 = y as Equivalence_Relation of X by A48;
      thus (the L_join of P1).(x,y) = x1 "\/" y1 by A43
                                   .= (the L_join of P2).(x,y) by A45;
     end;
       now let x,y be Element of Z;
      A49: x in Z & y in Z;
      then A50: ex x2 be Relation of X,X st x = x2 &
       x2 is Equivalence_Relation of X by A42;
        ex x3 be Relation of X,X st y = x3 &
       x3 is Equivalence_Relation of X by A42,A49;
      then reconsider x1 = x , y1 = y as Equivalence_Relation of X by A50;
      thus (the L_meet of P1).(x,y) = x1 /\ y1 by A43
                                   .= (the L_meet of P2).(x,y) by A45;
     end;
     then the L_meet of P1 = the L_meet of P2 by A42,A44,BINOP_1:2;
     hence P1 = P2 by A42,A44,A46,BINOP_1:2;
   end;
  end;

begin
     :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
     ::              MANY  SORTED  EQUIVALENCE  RELATIONS             ::
     :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

  definition
   let I,M;
   cluster MSEquivalence_Relation-like ManySortedRelation of M;
   existence
   proof
    deffunc F(set)=id (M.$1);
    consider f be ManySortedSet of I such that A1:
     for d st d in I holds
      f.d = F(d) from MSSLambda;
    A2: dom f = I by PBOOLE:def 3;
      for x be set st x in dom f holds f.x is Relation
    proof
     let x be set;
     assume x in dom f;
     then f.x = id (M.x) by A1,A2;
     hence thesis;
    end;
    then reconsider f as ManySortedRelation of I by MSUALG_4:def 1;
      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,M by MSUALG_4:def 2;
    reconsider f as ManySortedRelation of M;
    A3: 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 i in I & f.i = R;
     then R = id (M.i) by A1;
     hence thesis;
    end;
    take f;
    thus thesis by A3,MSUALG_4:def 3;
   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;
   func EqCl R -> Equivalence_Relation of M means
    :Def3: for i being 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 being Element of I holds EqR.i = F(i) from LambdaDMS;
      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 i' = i as Element of I;
       EqR.i = EqCl(R.i') by A1;
     hence thesis;
    end;
    then reconsider EqR as ManySortedRelation of M by MSUALG_4:def 2;
      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 A2: i in I & EqR.i = R1;
     then reconsider i' = i as Element of I;
       R1 = EqCl(R.i') by A1,A2;
     hence R1 is Equivalence_Relation of M.i;
    end;
    then reconsider EqR as Equivalence_Relation of M by MSUALG_4:def 3;
    take EqR;
    thus thesis by A1;
   end;
   uniqueness
   proof
    let C1,C2 be Equivalence_Relation of M such that
     A3: for i being Element of I holds C1.i = EqCl(R.i) and
     A4: for i being Element of I holds C2.i = EqCl(R.i);
       now let i; assume i in I;
      then reconsider i1 = i as Element of I;
      thus C1.i = EqCl(R.i1) by A3
               .= C2.i by A4;
     end;
     hence C1 = C2 by PBOOLE:3;
   end;
  end;

  theorem
     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 3;
     thus EqR.i = EqCl ER by Th3
               .= EqCl (EqR.i);
    end;
    hence thesis by Def3;
   end;

begin
     :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
     ::       LATTICE  OF  MANY  SORTED  EQUIVALENCE  RELATIONS       ::
     :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

  definition
   let I be non empty set,
       M be ManySortedSet of I;
   let EqR1,EqR2 be Equivalence_Relation of M;
   func EqR1 "\/" EqR2 -> Equivalence_Relation of M means
    :Def4: ex EqR3 being ManySortedRelation of M st EqR3 = EqR1 \/ EqR2 &
      it = EqCl EqR3;
   existence
   proof
    deffunc F(set) = (EqR1 \/ EqR2).$1;
    consider E be ManySortedSet of I such that A1:
     for i st i in I holds E.i = F(i) from MSSLambda;
      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 i' = i as Element of I;
       E.i = (EqR1 \/ EqR2).i by A1,A2
        .= EqR1.i' \/ EqR2.i' by PBOOLE:def 7;
     hence thesis;
    end;
    then reconsider E as ManySortedRelation of M by MSUALG_4:def 2;
    take EqCl E;
    take E;
    thus thesis by A1,PBOOLE:3;
   end;
   uniqueness;
   commutativity;
  end;

  theorem Th6:
   EqR1 \/ EqR2 c= EqR1 "\/" EqR2
   proof
    consider EqR3 being ManySortedRelation of M such that A1:
     EqR3 = EqR1 \/ EqR2 & EqR1 "\/" EqR2 = EqCl EqR3 by Def4;
      now let i; assume i in I;
     then reconsider i' = i as Element of I;
       EqR3.i c= EqCl(EqR3.i') by Def1;
     hence EqR3.i c= (EqR1 "\/" EqR2).i by A1,Def3;
    end;
    hence thesis by A1,PBOOLE:def 5;
   end;

  theorem Th7:
   for EqR be Equivalence_Relation of M st
    EqR1 \/ EqR2 c= EqR holds EqR1 "\/" EqR2 c= EqR
   proof
    let EqR be Equivalence_Relation of M such that A1: EqR1 \/ EqR2 c= EqR;
    consider EqR3 being ManySortedRelation of M such that A2:
     EqR3 = EqR1 \/ EqR2 & EqR1 "\/" EqR2 = EqCl EqR3 by Def4;
      now let i; assume A3: i in I;
     then reconsider i' = i as Element of I;
       EqR.i' is Relation of M.i;
     then reconsider E = EqR.i as Equivalence_Relation of M.i
                                                          by MSUALG_4:def 3;
       EqR3.i c= E by A1,A2,A3,PBOOLE:def 5;
     then EqCl(EqR3.i') c= E by Def1;
     hence (EqR1 "\/" EqR2).i c= EqR.i by A2,Def3;
    end;
    hence EqR1 "\/" EqR2 c= EqR by PBOOLE:def 5;
   end;

  theorem Th8:
   ( 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;
      EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by Th6;
    then A3: EqR3 c= EqR1 "\/" EqR2 by A2;
      EqR1 "\/" EqR2 c= EqR3 by A1,Th7;
    hence EqR3 = EqR1 "\/" EqR2 by A3,PBOOLE:def 13;
   end;

  theorem
     EqR "\/" EqR = EqR
   proof
      for EqR3 st EqR \/ EqR c= EqR3 holds EqR c= EqR3;
    hence thesis by Th8;
   end;

  theorem Th10:
   (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3)
   proof
      for EqR4 holds EqR4 = (EqR1 "\/" EqR2) "\/" EqR3 implies
     EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4
    proof
     let EqR4;
     A1: EqR1 "\/" EqR2 c= (EqR1 "\/" EqR2) \/ EqR3 by PBOOLE:16;
     A2: EqR3 c= (EqR1 "\/" EqR2) \/ EqR3 by PBOOLE:16;
     A3: EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by Th6;
     A4: EqR1 c= EqR1 \/ EqR2 & EqR2 c= EqR1 \/ EqR2 by PBOOLE:16;
     assume EqR4 = (EqR1 "\/" EqR2) "\/" EqR3;
     then A5: (EqR1 "\/" EqR2) \/ EqR3 c= EqR4 by Th6;
     then EqR1 "\/" EqR2 c= EqR4 by A1,PBOOLE:15;
     then EqR1 \/ EqR2 c= EqR4 by A3,PBOOLE:15;
     then A6: EqR1 c= EqR4 & EqR2 c= EqR4 & EqR3 c= EqR4
                                                       by A2,A4,A5,PBOOLE:15;
     then EqR2 \/ EqR3 c= EqR4 by PBOOLE:18;
     then EqR2 "\/" EqR3 c= EqR4 by Th7;
     then EqR1 \/ (EqR2 "\/" EqR3) c= EqR4 by A6,PBOOLE:18;
     hence EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4 by Th7;
    end;
    then A7: EqR1 "\/" (EqR2 "\/" EqR3) c= (EqR1 "\/" EqR2) "\/" EqR3;
      for EqR4 holds EqR4 = EqR1 "\/" (EqR2 "\/" EqR3) implies
     (EqR1 "\/" EqR2) "\/" EqR3 c= EqR4
    proof
     let EqR4;
     A8: EqR2 "\/" EqR3 c= EqR1 \/ (EqR2 "\/" EqR3) by PBOOLE:16;
     A9: EqR1 c= EqR1 \/ (EqR2 "\/" EqR3) by PBOOLE:16;
     A10: EqR2 \/ EqR3 c= EqR2 "\/" EqR3 by Th6;
     A11: EqR2 c= EqR2 \/ EqR3 & EqR3 c= EqR2 \/ EqR3 by PBOOLE:16;
     assume EqR4 = EqR1 "\/" (EqR2 "\/" EqR3);
     then A12: EqR1 \/ (EqR2 "\/" EqR3) c= EqR4 by Th6;
     then EqR2 "\/" EqR3 c= EqR4 by A8,PBOOLE:15;
     then EqR2 \/ EqR3 c= EqR4 by A10,PBOOLE:15;
     then A13: EqR1 c= EqR4 & EqR2 c= EqR4 & EqR3 c= EqR4
                                                       by A9,A11,A12,PBOOLE:15;
     then EqR1 \/ EqR2 c= EqR4 by PBOOLE:18;
     then EqR1 "\/" EqR2 c= EqR4 by Th7;
     then (EqR1 "\/" EqR2) \/ EqR3 c= EqR4 by A13,PBOOLE:18;
     hence (EqR1 "\/" EqR2) "\/" EqR3 c= EqR4 by Th7;
    end;
    then (EqR1 "\/" EqR2) "\/" EqR3 c= EqR1 "\/" (EqR2 "\/" EqR3);
    hence thesis by A7,PBOOLE:def 13;
   end;

  theorem Th11:
   EqR1 /\ (EqR1 "\/" EqR2) = EqR1
   proof
    thus EqR1 /\ (EqR1 "\/" EqR2) c= EqR1 by PBOOLE:17;
    A1: EqR1 c= EqR1 \/ EqR2 by PBOOLE:16;
      EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by Th6;
    then EqR1 c= EqR1 "\/" EqR2 by A1,PBOOLE:15;
    hence EqR1 c= EqR1 /\ (EqR1 "\/" EqR2) by PBOOLE:19;
   end;

  theorem Th12:
   for EqR be Equivalence_Relation of M st EqR = EqR1 /\ EqR2 holds
    EqR1 "\/" EqR = EqR1
   proof
    let EqR be Equivalence_Relation of M such that A1: EqR = EqR1 /\ EqR2;
    A2: EqR1 = EqR1 \/ (EqR1 /\ EqR2) by PBOOLE:37;
      for EqR4 st EqR1 \/ (EqR1 /\ EqR2) c= EqR4 holds EqR1 c= EqR4 by PBOOLE:
37
;
    hence thesis by A1,A2,Th8;
   end;

  theorem Th13:
   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 U1' = EqR1.i as Relation of M.i,M.i by MSUALG_4:def 2;
     reconsider U2' = EqR2.i as Relation of M.i,M.i by A1,MSUALG_4:def 2;
       (EqR1 /\ EqR2).i = U1' /\ U2' by A1,PBOOLE:def 8;
     hence (EqR1 /\ EqR2).i is Relation of M.i,M.i;
    end;
    then reconsider U3 = EqR1 /\ EqR2 as ManySortedRelation of M
                                                          by MSUALG_4:def 2;
      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 A2: i in I & U3.i = R;
     then reconsider U1' = EqR1.i as Relation of M.i by MSUALG_4:def 2;
     reconsider U1' as Equivalence_Relation of M.i by A2,MSUALG_4:def 3;
     reconsider U2' = EqR2.i as Relation of M.i by A2,MSUALG_4:def 2;
     reconsider U2' as Equivalence_Relation of M.i by A2,MSUALG_4:def 3;
       U1' /\ U2' is Equivalence_Relation of M.i;
     hence R is Equivalence_Relation of M.i by A2,PBOOLE:def 8;
    end;
    hence EqR1 /\ EqR2 is Equivalence_Relation of M by MSUALG_4:def 3;
   end;

  definition
   let I be non empty set;
   let M be ManySortedSet of I;
   func EqRelLatt M -> strict Lattice means
    :Def5: (for x being set holds x in the carrier of it
     iff x is Equivalence_Relation of M) &
    for x,y being 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
    deffunc F(Element of I)=bool [:M.$1,M.$1:];
    consider M2 being ManySortedSet of I such that A1:
     for i be Element of I holds M2.i = F(i) from LambdaDMS;
    defpred P[set] means $1 is Equivalence_Relation of M;
    consider B be set such that A2: for x being set holds
     x in B iff x in product M2 & P[x] from Separation;
    A3: for EqR be Equivalence_Relation of M holds EqR in product M2
    proof
     let EqR be Equivalence_Relation of M;
     A4: dom EqR = I by PBOOLE:def 3
                .= dom M2 by PBOOLE:def 3;
       for x be set st x in dom M2 holds EqR.x in M2.x
     proof
      let x be set; assume x in dom M2;
      then reconsider x' = x as Element of I by PBOOLE:def 3;
      A5: M2.x' = bool [:M.x',M.x':] by A1;
        EqR.x' is Element of bool [:M.x',M.x':];
      hence EqR.x in M2.x by A5;
     end;
     hence EqR in product M2 by A4,CARD_3:18;
    end;
    consider f be Equivalence_Relation of M;
      f in product M2 by A3;
    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
      ex EqR3 being ManySortedRelation of M st EqR3 = x1 \/ y1 &
       $3 = EqCl EqR3);
    A6: for x,y being Element of B ex z being Element of B st Z[x,y,z]
    proof
     let x,y be Element of B;
     reconsider x' = x , y' = y as Equivalence_Relation of M by A2;
     set z = x' "\/" y';
       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 x1 = x & y1 = y;
     hence ex EqR3 being ManySortedRelation of M st EqR3 = x1 \/ y1 &
       z = EqCl EqR3 by Def4;
    end;
    consider B1 be BinOp of B such that A7:
     for x,y being Element of B
      holds Z[x,y,B1.(x,y)] from BinOpEx(A6);
    A8: now let x,y be Equivalence_Relation of M;
       x in product M2 & y in product M2 by A3;
     then reconsider x' = x , y' = y as Element of B by A2;
     consider EqR3 being ManySortedRelation of M such that A9:
      EqR3 = x \/ y & B1.(x',y') = EqCl EqR3 by A7;
     thus B1.(x,y) = x "\/" y by A9,Def4;
    end;
    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 being Element of B ex z being Element of B st Q[x,y,z]
    proof
     let x,y be Element of B;
     reconsider x' = x , y' = y as Equivalence_Relation of M by A2;
     set z = x' /\ y';
       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 i' = i as Element of I;
        z.i = x'.i' /\ y'.i' by PBOOLE:def 8;
      hence thesis;
     end;
     then reconsider z as ManySortedRelation of M by MSUALG_4:def 2;
       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 A11: i in I & z.i = R;
      then reconsider i' = i as Element of I;
      reconsider x1'' = x'.i' , y1'' = y'.i' as Relation of M.i;
      reconsider x'' = x1'' , y'' = y1'' as Equivalence_Relation of M.i
                                                       by MSUALG_4:def 3;
        R = x'' /\ y'' by A11,PBOOLE:def 8;
      hence thesis;
     end;
     then reconsider z as Equivalence_Relation of M by MSUALG_4:def 3;
       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 A12:
     for x,y being Element of B holds Q[x,y,B2.(x,y)] from BinOpEx(A10);
    A13: now let x,y be Equivalence_Relation of M;
       x in product M2 & y in product M2 by A3;
     then reconsider x' = x , y' = y as Element of B by A2;
       x' = x & y' = y;
     hence B2.(x,y) = x /\ y by A12;
    end;
    reconsider L = LattStr (# B,B1,B2 #) as non empty LattStr
      by STRUCT_0:def 1;
    A14: B1 is commutative
    proof
       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 A8
                   .= B1.(b,a) by A8;
     end;
     hence thesis by BINOP_1:def 2;
    end;
    A15: B1 is associative
    proof
       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 A8
                          .= U1 "\/" (U2 "\/" U3) by A8
                          .= (U1 "\/" U2) "\/" U3 by Th10
                          .= B1.(U1 "\/" U2,c) by A8
                          .= B1.(B1.(a,b),c) by A8;
     end;
     hence thesis by BINOP_1:def 3;
    end;
    A16:B2 is commutative
    proof
       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 A13
                   .= B2.(b,a) by A13;
     end;
     hence thesis by BINOP_1:def 2;
    end;
    A17: B2 is associative
    proof
       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 Th13;
      reconsider EQR2 = U1 /\ U2 as Equivalence_Relation of M by Th13;
      thus B2.(a,B2.(b,c)) = B2.(a,EQR1) by A13
                          .= U1 /\ (U2 /\ U3) by A13
                          .= (U1 /\ U2) /\ U3 by PBOOLE:35
                          .= B2.(EQR2,c) by A13
                          .= B2.(B2.(a,b),c) by A13;
     end;
     hence thesis by BINOP_1:def 3;
    end;
    A18: for a,b being 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 A14,BINOP_1:def 2
              .=b"\/"a by LATTICES:def 1;
    end;
    A19: for a,b,c being 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;
     A20: (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,BINOP_1:
def 3
              .=(a"\/"b)"\/"c by A20,LATTICES:def 1;
    end;
    A21: for a,b being 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;
     A22: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 Th13;
        B2.(x,y) = U1 /\ U2 by A13;
      hence B1.(B2.(x,y),y) = EQR "\/" U2 by A8
                           .= y by Th12;
     end;
     thus (a"/\"b)"\/"b = (the L_join of L).((a"/\"b),b) by LATTICES:def 1
           .= b by A22,LATTICES:def 2;
    end;
    A23: for a,b being 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 A16,BINOP_1:def 2
              .=b"/\"a by LATTICES:def 2;
    end;
    A24: for a,b,c being 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;
     A25: (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 A17,BINOP_1:
def 3
              .=(a"/\"b)"/\"c by A25,LATTICES:def 2;
    end;
      for a,b being 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;
     A26: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 A8;
      hence B2.(x,B1.(x,y)) = (U1 /\( U1 "\/" U2)) by A13
                           .= x by Th11;
     end;
     thus a"/\"(a"\/"b) = (the L_meet of L).(a,(a"\/"b)) by LATTICES:def 2
           .= a by A26,LATTICES:def 1;
    end;
    then L is join-commutative join-associative meet-absorbing
          meet-commutative meet-associative join-absorbing
    by A18,A19,A21,A23,A24,LATTICES:def 4,def 5,def 6,def 7,def 8,def 9;
    then reconsider L as strict Lattice by LATTICES:def 10;
    take L;
    thus for x being set holds x in the carrier of L
     iff x is Equivalence_Relation of M
    proof
     let x be set;
     thus x in the carrier of L implies x is Equivalence_Relation of M by A2;
     thus x is Equivalence_Relation of M implies x in the carrier of L
     proof
      assume A27: x is Equivalence_Relation of M;
      then x in product M2 by A3;
      hence x in the carrier of L by A2,A27;
     end;
    end;
    thus thesis by A8,A13;
   end;
   uniqueness
   proof
    let S1,S2 be strict Lattice such that
    A28: for x being set holds x in the carrier of S1
      iff x is Equivalence_Relation of M and
    A29: for x,y being Equivalence_Relation of M holds
      (the L_meet of S1).(x,y) = x /\ y &
      (the L_join of S1).(x,y) = x "\/" y and
    A30: for x being set holds x in the carrier of S2
      iff x is Equivalence_Relation of M and
    A31: for x,y being Equivalence_Relation of M holds
      (the L_meet of S2).(x,y) = x /\ y &
      (the L_join of S2).(x,y) = x "\/" y;
    A32: now let x be set;
       x is Equivalence_Relation of M iff x in the carrier of S2 by A30;
     hence x in the carrier of S1 iff x in the carrier of S2 by A28;
    end;
    then A33: the carrier of S1 = the carrier of S2 by TARSKI:2;
    reconsider Z = the carrier of S1 as non empty set;
      now let x,y be Element of Z;
     reconsider x1 = x , y1 = y as Equivalence_Relation of M by A28;
     thus (the L_meet of S1).(x,y) = x1 /\ y1 by A29
                                  .= (the L_meet of S2).(x,y) by A31;
     thus (the L_join of S1).(x,y) = x1 "\/" y1 by A29
                                  .= (the L_join of S2).(x,y) by A31;
    end;
    then the L_meet of S1 = the L_meet of S2 &
         the L_join of S1 = the L_join of S2 by A33,BINOP_1:2;
    hence S1 = S2 by A32,TARSKI:2;
   end;
  end;

begin
     :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
     ::    LATTICE  OF  CONGRUENCES  IN  A  MANY  SORTED  ALGEBRA     ::
     :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

  definition
   let S be non empty ManySortedSign;
   let A be MSAlgebra over S;
   cluster MSEquivalence-like ->
          MSEquivalence_Relation-like ManySortedRelation of A;
   coherence by MSUALG_4:def 5;
  end;

  reserve S for non void non empty ManySortedSign;
  reserve A for non-empty MSAlgebra over S;

  theorem Th14:
   for o be OperSymbol of S
   for C1,C2 being MSCongruence of A
   for x1,y1 be set
   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 A2:
     x = (a1 ^ <*x1*> ^ b1) & y = (a1 ^ <*y1*> ^ b1);
    then A3: x = a1 ^ (<*x1*> ^ b1) & y = a1 ^ (<*y1*> ^ b1) by FINSEQ_1:45;
      now per cases by A1,XBOOLE_0:def 2;
     suppose A4: [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 A5: n in dom x;
       then A6: n in dom (a1 ^ <*x1*>) or (ex k be Nat st k in dom b1 &
        n = len (a1 ^ <*x1*>) + k) by A2,FINSEQ_1:38;
       A7: the OperSymbols of S is non empty set by MSUALG_1:def 5;
       A8: n in dom (the_arity_of o) by A5,MSUALG_3:6;
       then A9: n in dom ((the Sorts of A) * (the_arity_of o))
                                              by PBOOLE:def 3;
       reconsider dz = dom (the_arity_of o) as non empty set by A5,MSUALG_3:6;
       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 9
         .= pi((the Sorts of A)# . ((the Arity of S).o),n) by A7,FUNCT_2:21
         .= pi((the Sorts of A)# . (the_arity_of o),n) by MSUALG_1:def 6
         .= pi(product((the Sorts of A) * (the_arity_of o)),n)
                                                           by MSUALG_1:def 3
         .= ((the Sorts of A) * (the_arity_of o)).n by A9,A10,CARD_3:22
         .= (the Sorts of A) . ((the_arity_of o).n) by A8,FUNCT_1:23
         .= (the Sorts of A) . ((the_arity_of o)/.n) by A8,FINSEQ_4:def 4;
    then A11: x.n in (the Sorts of A).((the_arity_of o)/.n) by CARD_3:def 6;
         now per cases by A6,FINSEQ_1:38;
        suppose A12: n in dom a1;
         then A13: x.n = a1.n by A3,FINSEQ_1:def 7;
            y.n = a1.n by A3,A12,FINSEQ_1:def 7;
         hence [x.n,y.n] in C1.((the_arity_of o)/.n) by A11,A13,EQREL_1:11;
        suppose ex m be Nat st m in dom <*x1*> & n = len a1 + m;
         then consider m be Nat such that A14: m in
 dom <*x1*> & n = len a1 + m;
         A15: m in Seg 1 by A14,FINSEQ_1:55;
         then A16: m = 1 by FINSEQ_1:4,TARSKI:def 1;
         then A17: n in Seg (len a1 + 1) by A14,FINSEQ_1:6;
         then n in Seg (len a1 + len <*x1*>) by FINSEQ_1:57;
         then n in Seg len (a1 ^ <*x1*>) by FINSEQ_1:35;
         then A18: n in dom (a1 ^ <*x1*>) by FINSEQ_1:def 3;
           n in Seg (len a1 + len <*y1*>) by A17,FINSEQ_1:57;
         then n in Seg len (a1 ^ <*y1*>) by FINSEQ_1:35;
         then A19: n in dom (a1 ^ <*y1*>) by FINSEQ_1:def 3;
         A20: x.n = (a1 ^ <*x1*>).(len a1 + 1) by A2,A14,A16,A18,FINSEQ_1:def 7
                .= x1 by FINSEQ_1:59;
           y.n = (a1 ^ <*y1*>).(len a1 + 1) by A2,A14,A16,A19,FINSEQ_1:def 7
            .= y1 by FINSEQ_1:59;
         hence [x.n,y.n] in C1.((the_arity_of o)/.n)
                                   by A4,A14,A15,A20,FINSEQ_1:4,TARSKI:def 1;
        suppose ex k be Nat st k in dom b1 & n = len (a1 ^ <*x1*>) + k;
         then consider k be Nat such that A21:
          k in dom b1 & n = len (a1 ^ <*x1*>) + k;
         A22: x.n = b1.k by A2,A21,FINSEQ_1:def 7;
           n = len a1 + len <*x1*> + k by A21,FINSEQ_1:35;
         then n = len a1 + 1 + k by FINSEQ_1:57;
         then n = len a1 + len <*y1*> + k by FINSEQ_1:57;
         then n = len (a1 ^ <*y1*>) + k by FINSEQ_1:35;
         then y.n = b1.k by A2,A21,FINSEQ_1:def 7;
         hence [x.n,y.n] in C1.((the_arity_of o)/.n) by A11,A22,EQREL_1:11;
       end;
       hence thesis;
      end;
      then [Den(o,A).x,Den(o,A).y] in
                                C1.(the_result_sort_of o) by MSUALG_4:def 6;
      hence [Den(o,A).x,Den(o,A).y] in
            C1.(the_result_sort_of o) \/
 C2.(the_result_sort_of o) by XBOOLE_0:def 2;
     suppose A23: [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 A24: n in dom x;
       then A25: n in dom (a1 ^ <*x1*>) or (ex k be Nat st k in dom b1 &
        n = len (a1 ^ <*x1*>) + k) by A2,FINSEQ_1:38;
       A26: the OperSymbols of S is non empty set by MSUALG_1:def 5;
       A27: n in dom (the_arity_of o) by A24,MSUALG_3:6;
       then A28: n in dom ((the Sorts of A) * (the_arity_of o))
                                              by PBOOLE:def 3;
       reconsider dz = dom (the_arity_of o) as non empty set by A24,MSUALG_3:6;
       reconsider so = (the Sorts of A) * (the_arity_of o) as
                                               non-empty ManySortedSet of dz;
       A29: 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 9
         .= pi((the Sorts of A)# . ((the Arity of S).o),n) by A26,FUNCT_2:21
         .= pi((the Sorts of A)# . (the_arity_of o),n) by MSUALG_1:def 6
         .= pi(product((the Sorts of A) * (the_arity_of o)),n)
                                                           by MSUALG_1:def 3
         .= ((the Sorts of A) * (the_arity_of o)).n by A28,A29,CARD_3:22
         .= (the Sorts of A) . ((the_arity_of o).n) by A27,FUNCT_1:23
         .= (the Sorts of A) . ((the_arity_of o)/.n) by A27,FINSEQ_4:def 4;
       then A30: x.n in (the Sorts of A).((the_arity_of o)/.n) by CARD_3:def 6;
         now per cases by A25,FINSEQ_1:38;
        suppose A31: n in dom a1;
         then A32: x.n = a1.n by A3,FINSEQ_1:def 7;
            y.n = a1.n by A3,A31,FINSEQ_1:def 7;
         hence [x.n,y.n] in C2.((the_arity_of o)/.n) by A30,A32,EQREL_1:11;
        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*> & n = len a1 + m;
         A34: m in Seg 1 by A33,FINSEQ_1:55;
         then A35: m = 1 by FINSEQ_1:4,TARSKI:def 1;
         then A36: n in Seg (len a1 + 1) by A33,FINSEQ_1:6;
         then n in Seg (len a1 + len <*x1*>) by FINSEQ_1:57;
         then n in Seg len (a1 ^ <*x1*>) by FINSEQ_1:35;
         then A37: n in dom (a1 ^ <*x1*>) by FINSEQ_1:def 3;
           n in Seg (len a1 + len <*y1*>) by A36,FINSEQ_1:57;
         then n in Seg len (a1 ^ <*y1*>) by FINSEQ_1:35;
         then A38: n in dom (a1 ^ <*y1*>) by FINSEQ_1:def 3;
         A39: x.n = (a1 ^ <*x1*>).(len a1 + 1) by A2,A33,A35,A37,FINSEQ_1:def 7
                .= x1 by FINSEQ_1:59;
           y.n = (a1 ^ <*y1*>).(len a1 + 1) by A2,A33,A35,A38,FINSEQ_1:def 7
            .= y1 by FINSEQ_1:59;
         hence [x.n,y.n] in C2.((the_arity_of o)/.n)
                                   by A23,A33,A34,A39,FINSEQ_1:4,TARSKI:def 1;
        suppose ex k be Nat st k in dom b1 & n = len (a1 ^ <*x1*>) + k;
         then consider k be Nat such that A40:
          k in dom b1 & n = len (a1 ^ <*x1*>) + k;
         A41: x.n = b1.k by A2,A40,FINSEQ_1:def 7;
           n = len a1 + len <*x1*> + k by A40,FINSEQ_1:35;
         then n = len a1 + 1 + k by FINSEQ_1:57;
         then n = len a1 + len <*y1*> + k by FINSEQ_1:57;
         then n = len (a1 ^ <*y1*>) + k by FINSEQ_1:35;
         then y.n = b1.k by A2,A40,FINSEQ_1:def 7;
         hence [x.n,y.n] in C2.((the_arity_of o)/.n) by A30,A41,EQREL_1:11;
       end;
       hence thesis;
      end;
      then [Den(o,A).x,Den(o,A).y] in C2.(the_result_sort_of o)
                                                          by MSUALG_4:def 6;
      hence [Den(o,A).x,Den(o,A).y] in C1.(the_result_sort_of o) \/
 C2.(the_result_sort_of o) by XBOOLE_0:def 2;
    end;
    hence [Den(o,A).x,Den(o,A).y] in
                       C1.(the_result_sort_of o) \/ C2.(the_result_sort_of o);
   end;

  theorem Th15:
   for o be OperSymbol of S
   for C1,C2 being MSCongruence of A
   for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2
   for x1,y1 be set
   for n be Nat
   for a1,a2,b1 being FinSequence st len a1 = n & len a1 = len a2 &
    for k be 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;
   let x1,y1 be set;
   let n be Nat;
   let a1,a2,b1 be FinSequence such that A2:
    len a1 = n & len a1 = len a2 &
    for k be Nat st k in dom a1 holds [a1.k,a2.k] in C.((the_arity_of o)/.k);
   assume that A3: [Den(o,A).(a1 ^ <*x1*> ^ b1),Den(o,A).(a2 ^ <*x1*> ^ b1)] in
                                                 C.(the_result_sort_of o) and
               A4: [x1,y1] in C.((the_arity_of o)/.(n+1));
   let x be Element of Args(o,A) such that A5: x = a1 ^ <*x1*> ^ b1;
   set y = a2 ^ <*y1*> ^ b1;
   A6: the OperSymbols of S is non empty set by MSUALG_1:def 5;
   A7: dom x = Seg len (a1 ^ <*x1*> ^ b1) by A5,FINSEQ_1:def 3
            .= Seg len (a1 ^ (<*x1*> ^ b1)) by FINSEQ_1:45
            .= Seg (len a2 + len (<*x1*> ^ b1)) by A2,FINSEQ_1:35
            .= Seg len (a2 ^ (<*x1*> ^ b1)) by FINSEQ_1:35
            .= Seg len (a2 ^ <*x1*> ^ b1) by FINSEQ_1:45
            .= dom (a2 ^ <*x1*> ^ b1) by FINSEQ_1:def 3;
   consider C' being ManySortedRelation of the Sorts of A such that A8:
    C' = C1 \/ C2 & C1 "\/" C2 = EqCl C' by Def4;
   A9: 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 Th2
      .= EqCl (C'.(the_result_sort_of o)) by A8,PBOOLE:def 7
      .= (C1 "\/" C2).(the_result_sort_of o) by A8,Def3;
   A10: (the Sorts of A).(the_result_sort_of o) =
                (the Sorts of A).((the ResultSort of S).o) by MSUALG_1:def 7
             .= ((the Sorts of A) * the ResultSort of S).o by A6,FUNCT_2:21
             .= Result(o,A) by MSUALG_1:def 10;
   then Den(o,A).x in (the Sorts of A).(the_result_sort_of o);
   then consider p be FinSequence such that A11: 1 <= len p &
   Den(o,A).(a1 ^ <*x1*> ^ b1) = p.1 & Den(o,A).(a2 ^ <*x1*> ^ b1) = p.(len p)
    & 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,A3,A5,A9,EQREL_1:36;
   consider D' being ManySortedRelation of the Sorts of A such that A12:
    D' = C1 \/ C2 & C1 "\/" C2 = EqCl D' by Def4;
   A13: 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 Th2
         .= EqCl (D'.((the_arity_of o)/.(n+1))) by A12,PBOOLE:def 7
         .= (C1 "\/" C2).((the_arity_of o)/.(n+1)) by A12,Def3;
     x1 in (the Sorts of A).((the_arity_of o)/.(n+1)) by A4,ZFMISC_1:106;
   then consider f be FinSequence such that A14: 1 <= len f & x1 = f.1 &
   y1 = f.(len f) & 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,A4,A13,EQREL_1:36;
   deffunc G(Nat)=Den(o,A).(a2 ^ <*f.$1*> ^ b1);
   consider g be FinSequence such that A15: len g = len f &
    for i be Nat st i in Seg len f holds g.i = G(i)
                                                              from SeqLambda;
     ex q being 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;
    A16: len q = len p + len g by FINSEQ_1:35;
    hence 1 <= len q by A11,NAT_1:37;
      1 in dom p by A11,FINSEQ_3:27;
    hence q.1 = Den(o,A).x by A5,A11,FINSEQ_1:def 7;
    A17: len g in Seg len f by A14,A15,FINSEQ_1:3;
    then len g in dom g by A15,FINSEQ_1:def 3;
    hence q.(len q) = g.len g by A16,FINSEQ_1:def 7
                  .= Den(o,A).y by A14,A15,A17;
    A18: len p <> 0 by A11;
    hereby let i be Nat such that A19: 1 <= i & i < len q;
     A20: (1 <= i & i < len p) or (len p + 1 <= i & i < len q) or i = len p
     proof
      assume that A21: not (1 <= i & i < len p) and
                  A22: not (len p + 1 <= i & i < len q);
        i <= len p by A19,A22,NAT_1:38;
      hence i = len p by A19,A21,AXIOMS:21;
     end;
     consider i1 be Nat such that A23: len p = i1 + 1 by A18,NAT_1:22;
     A24: Seg len (a1 ^ <*x1*> ^ b1) = dom x by A5,FINSEQ_1:def 3
                 .= dom (the_arity_of o) by MSUALG_3:6
                 .= Seg len (the_arity_of o) by FINSEQ_1:def 3;
     A25: len (a2 ^ <*x1*> ^ b1) = len (a2 ^ (<*x1*> ^ b1)) by FINSEQ_1:45
                 .= len a2 + len (<*x1*> ^ b1) by FINSEQ_1:35
                 .= len (a1 ^ (<*x1*> ^ b1)) by A2,FINSEQ_1:35
                 .= len (a1 ^ <*x1*> ^ b1) by FINSEQ_1:45
                 .= len the_arity_of o by A24,FINSEQ_1:8;
     A26: now let k be Nat; assume k in dom x;
      then A27: k in Seg len (the_arity_of o) by A7,A25,FINSEQ_1:def 3;
      then A28: k in dom (the_arity_of o) by FINSEQ_1:def 3;
      then A29: k in dom ((the Sorts of A) * (the_arity_of o))
                                              by PBOOLE:def 3;
      reconsider dz = dom (the_arity_of o) as non empty set
                                                      by A27,FINSEQ_1:def 3;
      reconsider so = (the Sorts of A) * (the_arity_of o) as
                                               non-empty ManySortedSet of dz;
      A30: 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 9
          .= pi((the Sorts of A)# . ((the Arity of S).o),k) by A6,FUNCT_2:21
          .= pi((the Sorts of A)# . (the_arity_of o),k) by MSUALG_1:def 6
          .= pi(product((the Sorts of A) * (the_arity_of o)),k)
                                                           by MSUALG_1:def 3
          .= ((the Sorts of A) * (the_arity_of o)).k by A29,A30,CARD_3:22
          .= (the Sorts of A) . ((the_arity_of o).k) by A28,FUNCT_1:23
          .= (the Sorts of A) . ((the_arity_of o)/.k) by A28,FINSEQ_4:def 4;
      hence x.k in (the Sorts of A).((the_arity_of o)/.k) by CARD_3:def 6;
     end;
       now per cases by A20;
      suppose A31: 1 <= i & i < len p;
       then i in dom p by FINSEQ_3:27;
       then A32: q.i = p.i by FINSEQ_1:def 7;
         1 <= i+1 & i+1 <= len p by A31,NAT_1:38;
       then i+1 in dom p by FINSEQ_3:27;
       then q.(i+1) = p.(i+1) 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 A11,A31,A32;
      suppose A33: i = len p;
       then i in Seg len p by A23,FINSEQ_1:6;
       then i in dom p by FINSEQ_1:def 3;
       then A34: q.i = Den(o,A).(a2 ^ <*x1*> ^ b1) by A11,A33,FINSEQ_1:def 7;
       A35: 1 in Seg len g by A14,A15,FINSEQ_1:3;
       then 1 in dom g by FINSEQ_1:def 3;
       then A36: q.(i+1) = g.1 by A33,FINSEQ_1:def 7
                        .= Den(o,A).(a2 ^ <*x1*> ^ b1) by A14,A15,A35;
         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 A37: k in dom (a2 ^ <*x1*> ^ b1);
        then A38: k in dom (a2 ^ (<*x1*> ^ b1)) by FINSEQ_1:45;
          now per cases by A38,FINSEQ_1:38;
         suppose A39: k in dom a2;
          then k in Seg len a2 by FINSEQ_1:def 3;
          then k in dom a1 by A2,FINSEQ_1:def 3;
          then A40: [a1.k,a2.k] in C.((the_arity_of o)/.k) by A2;
            (a2 ^ <*x1*> ^ b1).k = (a2 ^ (<*x1*> ^ b1)).k by FINSEQ_1:45
                 .= a2.k by A39,FINSEQ_1:def 7;
          hence (a2 ^ <*x1*> ^ b1).k in (the Sorts of A).((the_arity_of o)/.k)
                                                  by A40,ZFMISC_1:106;
         suppose ex n1 be Nat st n1 in dom (<*x1*> ^ b1) & k = len a2 + n1;
          then consider n1 be Nat such that
           A41: n1 in dom (<*x1*> ^ b1) & k = len a2 + n1;
            (a2 ^ <*x1*> ^ b1).k = (a2 ^ (<*x1*> ^ b1)).k by FINSEQ_1:45
                           .= (<*x1*> ^ b1).n1 by A41,FINSEQ_1:def 7
                           .= (a1 ^ (<*x1*> ^ b1)).k by A2,A41,FINSEQ_1:def 7
                           .= x.k by A5,FINSEQ_1:45;
         hence (a2 ^ <*x1*> ^ b1).k in (the Sorts of A).((the_arity_of o)/.k)
                                                               by A7,A26,A37;
        end;
        hence (a2 ^ <*x1*> ^ b1).k in (the Sorts of A).((the_arity_of o)/.k);
       end;
       then reconsider de = (a2 ^ <*x1*> ^ b1) as Element of Args(o,A)
         by A25,MSAFREE2:7;
       A42: Den(o,A).de in (the Sorts of A).(the_result_sort_of o) by A10;
         field (C1.(the_result_sort_of o)) =
                                    (the Sorts of A).(the_result_sort_of o) &
       field (C2.(the_result_sort_of o)) =
                       (the Sorts of A).(the_result_sort_of o) by EQREL_1:16;
       then A43: 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
RELAT_1:33
           .= (the Sorts of A).(the_result_sort_of o);
       C1.(the_result_sort_of o) \/ C2.(the_result_sort_of o)
                                                  is reflexive by RELAT_2:31;
       then 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 A43,RELAT_2:def 9;
       hence [q.i,q.(i+1)] in C1.(the_result_sort_of o) \/
                      C2.(the_result_sort_of o) by A34,A36,A42,RELAT_2:def 1;
      suppose A44: len p + 1 <= i & i < len q;
       then A45: len p + 1 <= i+1 by NAT_1:37;
       A46: i+1 <= len q by A44,NAT_1:38;
         len p < i by A44,NAT_1:38;
       then reconsider j = i - len p as Nat by EQREL_1:1;
       A47: 1 <= j by A44,REAL_1:84;
         len f = len q - len p by A15,A16,XCMPLX_1:26;
       then A48: j < len f by A44,REAL_1:54;
         1 <= j & j <= len f by A15,A16,A44,REAL_1:84;
       then A49: i - len p in Seg len f by FINSEQ_1:3;
         1 <= j+1 & j+1 <= len f by A48,NAT_1:37,38;
       then j+1 in Seg len f by FINSEQ_1:3;
       then A50: i + 1 - len p in Seg len f by XCMPLX_1:29;
       A51: [f.j,f.(j + 1)] in C1.((the_arity_of o)/.(n+1)) \/
 C2.((the_arity_of o)/.(n+1)) by A14,A47,A48;
       then A52: f.(i - len p) in (the Sorts of A).((the_arity_of o)/.(n+1))
                                            by ZFMISC_1:106;
       A53: f.(i - len p + 1) in (the Sorts of A).((the_arity_of o)/.(n+1))
                                        by A51,ZFMISC_1:106;
       A54: 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 A55: k in dom (a2 ^ <*f.(i - len p)*> ^ b1);
        then A56: 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:38;
          now per cases by A56,FINSEQ_1:38;
         suppose A57: k in dom a2;
          then k in Seg len a2 by FINSEQ_1:def 3;
          then k in dom a1 by A2,FINSEQ_1:def 3;
          then A58: [a1.k,a2.k] in C.((the_arity_of o)/.k) by A2;
            (a2 ^ <*f.(i - len p)*> ^ b1).k =
                          (a2 ^ (<*f.(i - len p)*> ^ b1)).k by FINSEQ_1:45
                          .= a2.k by A57,FINSEQ_1:def 7;
          hence (a2 ^ <*f.(i - len p)*> ^ b1).k in
             (the Sorts of A).((the_arity_of o)/.k) by A58,ZFMISC_1:106;
         suppose ex n2 be Nat st n2 in dom <*f.(i - len p)*> & k = len a2 + n2
;
          then consider n2 be Nat such that
           A59: n2 in dom <*f.(i - len p)*> & k = len a2 + n2;
          A60: n2 in Seg 1 by A59,FINSEQ_1:55;
          then A61: k = len a1 + 1 by A2,A59,FINSEQ_1:4,TARSKI:def 1;
          then k in Seg (len a2 + 1) by A2,FINSEQ_1:6;
          then k in Seg (len a2 + len <*f.(i - len p)*>) by FINSEQ_1:57;
          then k in Seg len (a2 ^ <*f.(i - len p)*>) by FINSEQ_1:35;
          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 A2,A61,FINSEQ_1:59;
          hence (a2 ^ <*f.(i - len p)*> ^ b1).k in
                             (the Sorts of A).((the_arity_of o)/.k)
                                    by A2,A52,A59,A60,FINSEQ_1:4,TARSKI:def 1;
         suppose ex n1 be Nat st n1 in dom b1 &
                                       k = len (a2 ^ <*f.(i - len p)*>) + n1;
          then consider n1 be Nat such that
           A62: n1 in dom b1 & k = len (a2 ^ <*f.(i - len p)*>) + n1;
          A63: len (a1 ^ <*x1*>) = len a1 + len <*x1*> by FINSEQ_1:35
                .= len a2 + 1 by A2,FINSEQ_1:57
                .= len a2 + len <*f.(i - len p)*> by FINSEQ_1:57
                .= len (a2 ^ <*f.(i - len p)*>) by FINSEQ_1:35;
          A64: dom x = Seg len (a1 ^ <*x1*> ^ b1) by A5,FINSEQ_1:def 3
            .= Seg (len (a1 ^ <*x1*>) + len b1) by FINSEQ_1:35
            .= Seg ((len a1 + len <*x1*>) + len b1) by FINSEQ_1:35
            .= Seg ((len a2 + 1) + len b1) by A2,FINSEQ_1:57
            .= Seg ((len a2 + len <*f.(i - len p)*>) + len b1) by FINSEQ_1:57
            .= Seg (len (a2 ^ <*f.(i - len p)*>) + len b1) by FINSEQ_1:35
            .= Seg len (a2 ^ <*f.(i - len p)*> ^ b1) by FINSEQ_1:35
            .= dom (a2 ^ <*f.(i - len p)*> ^ b1) by FINSEQ_1:def 3;
            (a2 ^ <*f.(i - len p)*> ^ b1).k = b1.n1 by A62,FINSEQ_1:def 7
                .= x.k by A5,A62,A63,FINSEQ_1:def 7;
          hence (a2 ^ <*f.(i - len p)*> ^ b1).k in
               (the Sorts of A).((the_arity_of o)/.k) by A26,A55,A64;
        end;
        hence (a2 ^ <*f.(i - len p)*> ^ b1).k in
                                       (the Sorts of A).((the_arity_of o)/.k);
       end;
       A65: 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 A66: k in dom (a2 ^ <*f.(i + 1 - len p)*> ^ b1);
        then A67: 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:38;
          now per cases by A67,FINSEQ_1:38;
         suppose A68: k in dom a2;
          then k in Seg len a2 by FINSEQ_1:def 3;
          then k in dom a1 by A2,FINSEQ_1:def 3;
          then A69: [a1.k,a2.k] in C.((the_arity_of o)/.k) by A2;
            (a2 ^ <*f.(i + 1 - len p)*> ^ b1).k =
                         (a2 ^ (<*f.(i + 1 - len p)*> ^ b1)).k by FINSEQ_1:45
                          .= a2.k by A68,FINSEQ_1:def 7;
          hence (a2 ^ <*f.(i + 1 - len p)*> ^ b1).k in
                      (the Sorts of A).
((the_arity_of o)/.k) by A69,ZFMISC_1:106;
         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
           A70: n2 in dom <*f.(i + 1 - len p)*> & k = len a2 + n2;
            n2 in Seg 1 by A70,FINSEQ_1:55;
          then A71: k = len a1 + 1 by A2,A70,FINSEQ_1:4,TARSKI:def 1;
          then k in Seg (len a2 + 1) by A2,FINSEQ_1:6;
          then k in Seg (len a2 + len <*f.(i + 1 - len p)*>) by FINSEQ_1:57;
          then k in Seg len (a2 ^ <*f.(i + 1 - len p)*>) by FINSEQ_1:35;
          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 A2,A71,FINSEQ_1:59;
          hence (a2 ^ <*f.(i + 1 - len p)*> ^ b1).k in
             (the Sorts of A).((the_arity_of o)/.k) by A2,A53,A71,XCMPLX_1:29
;
         suppose ex n1 be Nat st n1 in dom b1 &
                                   k = len (a2 ^ <*f.(i + 1 - len p)*>) + n1;
          then consider n1 be Nat such that
           A72: n1 in dom b1 & k = len (a2 ^ <*f.(i + 1 - len p)*>) + n1;
          A73: len (a1 ^ <*x1*>) = len a1 + len <*x1*> by FINSEQ_1:35
                .= len a2 + 1 by A2,FINSEQ_1:57
                .= len a2 + len <*f.(i + 1 - len p)*> by FINSEQ_1:57
                .= len (a2 ^ <*f.(i + 1 - len p)*>) by FINSEQ_1:35;
          A74: dom x = Seg len (a1 ^ <*x1*> ^ b1) by A5,FINSEQ_1:def 3
            .= Seg (len (a1 ^ <*x1*>) + len b1) by FINSEQ_1:35
            .= Seg ((len a1 + len <*x1*>) + len b1) by FINSEQ_1:35
            .= Seg ((len a2 + 1) + len b1) by A2,FINSEQ_1:57
            .= Seg ((len a2 + len <*f.(i + 1 - len p)*>) + len b1)
                                                               by FINSEQ_1:57
            .= Seg (len (a2 ^ <*f.(i + 1 - len p)*>) + len b1) by FINSEQ_1:35
            .= Seg len (a2 ^ <*f.(i + 1 - len p)*> ^ b1) by FINSEQ_1:35
            .= dom (a2 ^ <*f.(i + 1 - len p)*> ^ b1) by FINSEQ_1:def 3;
            (a2 ^ <*f.(i + 1 - len p)*> ^ b1).k = b1.n1 by A72,FINSEQ_1:def 7
                .= x.k by A5,A72,A73,FINSEQ_1:def 7;
          hence (a2 ^ <*f.(i + 1 - len p)*> ^ b1).k in
                           (the Sorts of A).
((the_arity_of o)/.k) by A26,A66,A74;
        end;
        hence (a2 ^ <*f.(i + 1 - len p)*> ^ b1).k in
                                (the Sorts of A).((the_arity_of o)/.k);
       end;
       A75: Seg len (a1 ^ <*x1*> ^ b1) = dom x by A5,FINSEQ_1:def 3
                 .= dom (the_arity_of o) by MSUALG_3:6
                 .= Seg len (the_arity_of o) by FINSEQ_1:def 3;
         len (a2 ^ <*f.(i - len p)*> ^ b1) = len the_arity_of o &
        len (a2 ^ <*f.(i + 1 - len p)*> ^ b1) = len the_arity_of o
       proof
        thus len (a2 ^ <*f.(i - len p)*> ^ b1) =
                   len (a2 ^ <*f.(i - len p)*>) + len b1 by FINSEQ_1:35
                .= len a2 + len <*f.(i - len p)*> + len b1 by FINSEQ_1:35
                .= len a2 + 1 + len b1 by FINSEQ_1:57
                .= len a1 + len <*x1*> + len b1 by A2,FINSEQ_1:57
                .= len (a1 ^ <*x1*>) + len b1 by FINSEQ_1:35
                .= len (a1 ^ <*x1*> ^ b1) by FINSEQ_1:35
                .= len the_arity_of o by A75,FINSEQ_1:8;
        thus len (a2 ^ <*f.(i + 1 - len p)*> ^ b1) =
                   len (a2 ^ <*f.(i + 1 - len p)*>) + len b1 by FINSEQ_1:35
                .= len a2 + len <*f.(i + 1 - len p)*> + len b1 by FINSEQ_1:35
                .= len a2 + 1 + len b1 by FINSEQ_1:57
                .= len a1 + len <*x1*> + len b1 by A2,FINSEQ_1:57
                .= len (a1 ^ <*x1*>) + len b1 by FINSEQ_1:35
                .= len (a1 ^ <*x1*> ^ b1) by FINSEQ_1:35
                .= len the_arity_of o by A75,FINSEQ_1:8;
       end;
       then reconsider d1 = a2 ^ <*f.(i - len p)*> ^ b1,
               d2 = a2 ^ <*f.(i + 1 - len p)*> ^ b1 as Element of Args(o,A)
                                                         by A54,A65,MSAFREE2:7;
       A76: q.i = g.(i - len p) by A16,A44,FINSEQ_1:36
              .= Den(o,A).d1 by A15,A49;
       A77: q.(i+1) = g.(i + 1 - len p) by A16,A45,A46,FINSEQ_1:36
                  .= Den(o,A).d2 by A15,A50;
         i + 1 - len p = i - len p + 1 by XCMPLX_1:29;
       then [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 A14,A47,A48;
       hence [q.i,q.(i+1)] in C1.(the_result_sort_of o) \/
                                 C2.(the_result_sort_of o) by A2,A76,A77,Th14;
     end;
     hence [q.i,q.(i+1)] in C1.(the_result_sort_of o) \/
                                                   C2.(the_result_sort_of o);
    end;
   end;
   hence [Den(o,A).x,Den(o,A).(a2 ^ <*y1*> ^ b1)] in C.(the_result_sort_of o)
                                                      by A1,A9,A10,EQREL_1:36;
  end;

  theorem Th16:
   for o be OperSymbol of S
   for C1,C2 being MSCongruence of A
   for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2
   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
   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);
   assume A2: for n be Nat st n in dom x holds
                                  [x.n,y.n] in C.((the_arity_of o)/.n);
   defpred P[Nat] means for a1,a2,b1 being 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));
   A3: P[0]
   proof
    let a1,a2,b1 be FinSequence;
    assume that
     A4: len a1 = 0 and
     A5: len a1 = len a2 and
     A6: 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);
     A7: a1 = {} & a2 = {} by A4,A5,FINSEQ_1:25;
    A8: the OperSymbols of S is non empty set by MSUALG_1:def 5;
    A9: (the Sorts of A).(the_result_sort_of o) =
                (the Sorts of A).((the ResultSort of S).o) by MSUALG_1:def 7
             .= ((the Sorts of A) * the ResultSort of S).o by A8,FUNCT_2:21
             .= Result(o,A) by MSUALG_1:def 10;
     field(C.(the_result_sort_of o))
          = (the Sorts of A).(the_result_sort_of o) by ORDERS_1:97;
      then C.(the_result_sort_of o) is_reflexive_in
                        (the Sorts of A).(the_result_sort_of o)
                 by RELAT_2:def 9;
    hence [Den(o,A).x,Den(o,A).(a2 ^ b1)] in C.(the_result_sort_of o)
                                                     by A6,A7,A9,RELAT_2:def 1;
   end;
   A10: for l be Nat st P[l] holds P[l+1]
   proof
    let l be Nat such that A11:
     for a1,a2,b1 being 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
     A12: len a1 = l+1 and
     A13: len a1 = len a2 and
     A14: x = a1 ^ b1 and
     A15: for n be Nat st n in dom a1 holds [x.n,(a2 ^ b1).n]
                                                in C.((the_arity_of o)/.n);
    set y = a2 ^ b1;
      a1 <> {} by A12,FINSEQ_1:25;
    then consider q1 be FinSequence, x1 be set such that A16: a1 = q1 ^ <*x1*>
                                                              by FINSEQ_1:63;
      a2 <> {} by A12,A13,FINSEQ_1:25;
    then consider q2 be FinSequence, y1 be set such that A17: a2 = q2 ^ <*y1*>
                                                              by FINSEQ_1:63;
    A18: l+1 = len q1 + len <*x1*> by A12,A16,FINSEQ_1:35
            .= len q1 + 1 by FINSEQ_1:57;
    then A19: len q1 = l by XCMPLX_1:2;
    A20: l+1 = len q2 + len <*y1*> by A12,A13,A17,FINSEQ_1:35
       .= len q2 + 1 by FINSEQ_1:57;
    then A21: len q1 = len q2 by A18,XCMPLX_1:2;
    A22: dom q1 = Seg len q1 by FINSEQ_1:def 3
              .= dom q2 by A21,FINSEQ_1:def 3;
    A23: for n be Nat st n in dom q1 holds [q1.n,q2.n] in
      C.((the_arity_of o)/.n)
    proof
     let n be Nat; assume A24: n in dom q1;
     then A25: n in Seg len q1 by FINSEQ_1:def 3;
       len q1 <= len a1 by A12,A18,NAT_1:29;
     then Seg len q1 c= Seg len a1 by FINSEQ_1:7;
     then n in Seg len a1 by A25;
     then A26: n in dom a1 by FINSEQ_1:def 3;
     then A27: x.n = a1.n by A14,FINSEQ_1:def 7
        .= q1.n by A16,A24,FINSEQ_1:def 7;
       dom a1 = Seg len a1 by FINSEQ_1:def 3
           .= dom a2 by A13,FINSEQ_1:def 3;
     then y.n = a2.n by A26,FINSEQ_1:def 7
             .= q2.n by A17,A22,A24,FINSEQ_1:def 7;
     hence [q1.n,q2.n] in C.((the_arity_of o)/.n) by A15,A26,A27;
    end;
    A28: [Den(o,A).x,Den(o,A).(q2 ^ <*x1*> ^ b1)] in C.(the_result_sort_of o)
    proof
     A29: q1 ^ <*x1*> ^ b1 = q1 ^ (<*x1*> ^ b1) by FINSEQ_1:45;
     A30: q2 ^ <*x1*> ^ b1 = q2 ^ (<*x1*> ^ b1) by FINSEQ_1:45;
       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 A31: n in dom q1;
      then A32: x.n = q1.n by A14,A16,A29,FINSEQ_1:def 7;
        (q2 ^ <*x1*> ^ b1).n = q2.n by A22,A30,A31,FINSEQ_1:def 7;
      hence [x.n,(q2 ^ <*x1*> ^ b1).n] in
      C.((the_arity_of o)/.n) by A23,A31,A32;
     end;
     hence [Den(o,A).x,Den(o,A).(q2 ^ <*x1*> ^ b1)] in
           C.(the_result_sort_of o) by A11,A14,A16,A19,A21,A29,A30;
    end;
    A33: l+1 in Seg len a1 by A12,FINSEQ_1:6;
    then A34: l+1 in dom a1 by FINSEQ_1:def 3;
    A35: l+1 in dom a2 by A13,A33,FINSEQ_1:def 3;
    A36: x1 = a1.(l + 1) by A16,A18,FINSEQ_1:59
          .= x.(l + 1) by A14,A34,FINSEQ_1:def 7;
       y1 = a2.(l + 1) by A17,A20,FINSEQ_1:59
           .= y.(l + 1) by A35,FINSEQ_1:def 7;
    then [x1,y1] in C.((the_arity_of o)/.(l+1)) by A15,A34,A36;
    hence [Den(o,A).x,Den(o,A).(a2 ^ b1)] in C.(the_result_sort_of o)
                                 by A1,A14,A16,A17,A18,A21,A23,A28,Th15;
   end;
   A37: for l be Nat holds P[l] from Ind(A3,A10);
   A38: dom x = dom (the_arity_of o) by MSUALG_3:6
            .= Seg len (the_arity_of o) by FINSEQ_1:def 3;
     dom y = 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 A38,FINSEQ_1:def 2;
   set b1 = {};
   A39: 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;
     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;
   then A40: len a1 = len a2 by A39,FINSEQ_1:8;
   A41: x = a1 ^ b1 by FINSEQ_1:47;
     y = a2 ^ b1 by FINSEQ_1:47;
   hence [Den(o,A).x,Den(o,A).y] in C.(the_result_sort_of o) by A2,A37,A40,A41
;
  end;

  theorem Th17:
   for C1,C2 being 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 5;
     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 Th16;
   hence C1 "\/" C2 is MSCongruence of A by MSUALG_4:def 6;
  end;

  theorem Th18:
   for C1,C2 being 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 Th13;
   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 5;
     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);
A2: 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 8;
     hence thesis by XBOOLE_0:def 3;
    end;
A3: 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 8;
     hence thesis by XBOOLE_0:def 3;
    end;
    A4: [Den(o,A).x,Den(o,A).y] in C1.(the_result_sort_of o)
                                                        by A2,MSUALG_4:def 6;
    A5: [Den(o,A).x,Den(o,A).y] in C2.(the_result_sort_of o)
                                                       by A3,MSUALG_4:def 6;
      C1.(the_result_sort_of o) /\ C2.(the_result_sort_of o) =
                                   C.(the_result_sort_of o) by PBOOLE:def 8;
    hence [Den(o,A).x,Den(o,A).y] in C.(the_result_sort_of o)
                                          by A4,A5,XBOOLE_0:def 3;
   end;
   hence C1 /\ C2 is MSCongruence of A by MSUALG_4:def 6;
  end;

  definition
   let S;
   let A be non-empty MSAlgebra over S;
   func CongrLatt A -> strict SubLattice of EqRelLatt the Sorts of A means
    :Def6: for x being set holds x in the carrier of it iff
      x is MSCongruence of A;
   existence
   proof
    deffunc F(Element of S)
        = bool [:(the Sorts of A).$1,(the Sorts of A).$1:];
    consider M2 being ManySortedSet of (the carrier of S) such that A1:
     for i be Element of (the carrier of S) holds M2.i =F(i) from LambdaDMS;
    defpred P[set] means $1  is MSCongruence of A;
    consider B be set such that A2: for x being set holds
     x in B iff x in product M2 & P[x] from Separation;
    A3: for C1 be MSCongruence of A holds C1 in product M2
    proof
     let C1 be MSCongruence of A;
     A4: dom C1 = the carrier of S by PBOOLE:def 3
               .= dom M2 by PBOOLE:def 3;
       now let x be set; assume x in dom M2;
      then reconsider x' = x as Element of (the carrier of S) by PBOOLE:def 3;
      A5: M2.x' = bool [:(the Sorts of A).x',(the Sorts of A).x':] by A1;
        C1.x' is Element of bool [:(the Sorts of A).x',(the Sorts of A).x':];
      hence C1.x in M2.x by A5;
     end;
     hence C1 in product M2 by A4,CARD_3:18;
    end;
    A6: for x being set holds x in B iff x is MSCongruence of A
    proof
     let x be set;
     thus x in B implies x is MSCongruence of A by A2;
     thus x is MSCongruence of A implies x in B
     proof
      assume A7: x is MSCongruence of A;
      then x in product M2 by A3;
      hence x in B by A2,A7;
     end;
    end;
    consider f be MSCongruence of A;
      f in B by A6;
    then reconsider B as non empty set;
    set D = the carrier of EqRelLatt the Sorts of A;
    set B1 = (the L_join of (EqRelLatt the Sorts of A)) | [:B,B:];
    set B2 = (the L_meet of (EqRelLatt the Sorts of A)) | [:B,B:];
    A8: B c= D
    proof
       now let x; 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;
     hence thesis by TARSKI:def 3;
    end;
    then [:B,B:] c= [:D,D:] by ZFMISC_1:119;
    then reconsider B1,B2 as Function of [:B,B:],D by FUNCT_2:38;
    A9: dom B1 = [:B,B:] by FUNCT_2:def 1;
      now let x be set; assume A10: x in [:B,B:];
     then consider x1,x2 be set such that A11: x = [x1,x2] by ZFMISC_1:102;
       x1 in B & x2 in B by A10,A11,ZFMISC_1:106;
     then reconsider x1' = x1 , x2' = x2 as MSCongruence of A by A6;
       x1' in B & x2' in B by A6;
     then [x1,x2] in [:B,B:] by ZFMISC_1:106;
     then B1.x = (the L_join of (EqRelLatt the Sorts of A)).[x1,x2] by A11,
FUNCT_1:72
     .= (the L_join of (EqRelLatt the Sorts of A)).(x1,x2) by BINOP_1:def 1
     .= x1' "\/" x2' by Def5;
     then B1.x is MSCongruence of A by Th17;
     hence B1.x in B by A6;
    end;
    then reconsider B1 as BinOp of B by A9,FUNCT_2:5;
    A12: dom B2 = [:B,B:] by FUNCT_2:def 1;
      now let x be set; assume A13: x in [:B,B:];
     then consider x1,x2 be set such that A14: x = [x1,x2] by ZFMISC_1:102;
       x1 in B & x2 in B by A13,A14,ZFMISC_1:106;
     then reconsider x1' = x1 , x2' = x2 as MSCongruence of A by A6;
       x1' in B & x2' in B by A6;
     then [x1,x2] in [:B,B:] by ZFMISC_1:106;
     then B2.x = (the L_meet of (EqRelLatt the Sorts of A)).[x1,x2] by A14,
FUNCT_1:72
     .= (the L_meet of (EqRelLatt the Sorts of A)).(x1,x2) by BINOP_1:def 1
     .= x1' /\ x2' by Def5;
     then B2.x is MSCongruence of A by Th18;
     hence B2.x in B by A6;
    end;
    then reconsider B2 as BinOp of B by A12,FUNCT_2:5;
    reconsider L = LattStr (# B,B1,B2 #) as non empty LattStr
      by STRUCT_0:def 1;
    A15: for a,b being MSCongruence of A holds
     B1.(a,b) = a "\/" b & B2.(a,b) = a /\ b
    proof
     let a,b be MSCongruence of A;
       a in B & b in B by A6;
     then A16: [a,b] in [:B,B:] by ZFMISC_1:106;
     thus B1.(a,b) = B1.[a,b] by BINOP_1:def 1
       .= (the L_join of (EqRelLatt the Sorts of A)).[a,b] by A16,FUNCT_1:72
       .= (the L_join of (EqRelLatt the Sorts of A)).(a,b) by BINOP_1:def 1
       .= a "\/" b by Def5;
     thus B2.(a,b) = B2.[a,b] by BINOP_1:def 1
       .= (the L_meet of (EqRelLatt the Sorts of A)).[a,b] by A16,FUNCT_1:72
       .= (the L_meet of (EqRelLatt the Sorts of A)).(a,b) by BINOP_1:def 1
       .= a /\ b by Def5;
    end;
    A17: B1 is commutative
    proof
       now let a,b be Element of B;
      reconsider a' = a , b' = b as MSCongruence of A by A6;
      thus B1.(a,b) = a' "\/" b' by A15
                   .= B1.(b,a) by A15;
     end;
     hence thesis by BINOP_1:def 2;
    end;
    A18: B1 is associative
    proof
       now let a,b,c be Element of B;
      reconsider a' = a , b' = b , c' = c as MSCongruence of A by A6;
      reconsider d = b' "\/" c' as MSCongruence of A by Th17;
      reconsider e = a' "\/" b' as MSCongruence of A by Th17;
      thus B1.(a,B1.(b,c)) = B1.(a,d) by A15
                          .= a' "\/" (b' "\/" c') by A15
                          .= (a' "\/" b') "\/" c' by Th10
                          .= B1.(e,c) by A15
                          .= B1.(B1.(a,b),c) by A15;
     end;
     hence thesis by BINOP_1:def 3;
    end;
    A19:B2 is commutative
    proof
       now let a,b be Element of B;
      reconsider a' = a , b' = b as MSCongruence of A by A6;
      thus B2.(a,b) = b' /\ a' by A15
                   .= B2.(b,a) by A15;
     end;
     hence thesis by BINOP_1:def 2;
    end;
    A20: B2 is associative
    proof
       now let a,b,c be Element of B;
      reconsider a' = a , b' = b , c' = c as MSCongruence of A by A6;
      reconsider e1 = b' /\ c' as MSCongruence of A by Th18;
      reconsider e2 = a' /\ b' as MSCongruence of A by Th18;
      thus B2.(a,B2.(b,c)) = B2.(a,e1) by A15
                          .= a' /\ (b' /\ c') by A15
                          .= (a' /\ b') /\ c' by PBOOLE:35
                          .= B2.(e2,c) by A15
                          .= B2.(B2.(a,b),c) by A15;
     end;
     hence thesis by BINOP_1:def 3;
    end;
    A21: for a,b being 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 A17,BINOP_1:def 2
              .= b"\/"a by LATTICES:def 1;
    end;
    A22: for a,b,c being 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 A18,BINOP_1:
def 3
              .= (the L_join of L).(a"\/"b,c) by LATTICES:def 1
              .= (a"\/"b)"\/"c by LATTICES:def 1;
    end;
    A23: for a,b being Element of L holds (a"/\"b)"\/"b = b
    proof let a,b be Element of L;
     A24: B1.(B2.(a,b),b)= b
     proof
      reconsider a' = a , b' = b as MSCongruence of A by A6;
      reconsider EQR = a' /\ b' as MSCongruence of A by Th18;
      thus B1.(B2.(a,b),b) = B1.(a' /\ b',b') by A15
                           .= EQR "\/" b' by A15
                           .= b by Th12;
     end;
     thus (a"/\"b)"\/"b = (the L_join of L).((a"/\"b),b) by LATTICES:def 1
           .= b by A24,LATTICES:def 2;
    end;
    A25: for a,b being 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 A19,BINOP_1:def 2
              .= b"/\"a by LATTICES:def 2;
    end;
    A26: for a,b,c being 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 A20,BINOP_1:
def 3
              .= (the L_meet of L).(a"/\"b,c) by LATTICES:def 2
              .= (a"/\"b)"/\"c by LATTICES:def 2;
    end;
      for a,b being Element of L holds a"/\"(a"\/"b)=a
    proof let a,b be Element of L;
     A27:B2.(a,B1.(a,b))= a
     proof
      reconsider a' = a , b' = b as MSCongruence of A by A6;
      reconsider d = a' "\/" b' as MSCongruence of A by Th17;
      thus B2.(a,B1.(a,b)) = B2.(a, d) by A15
                          .= (a' /\ ( a' "\/" b')) by A15
                          .= a by Th11;
     end;
     thus a"/\"(a"\/"b) = (the L_meet of L).(a,(a"\/"b)) by LATTICES:def 2
           .= a by A27,LATTICES:def 1;
    end;
    then L is join-commutative join-associative meet-absorbing
         meet-commutative meet-associative join-absorbing
    by A21,A22,A23,A25,A26,LATTICES:def 4,def 5,def 6,def 7,def 8,def 9;
    then reconsider L as Lattice by LATTICES:def 10;
    reconsider L as strict SubLattice of EqRelLatt the Sorts of A
                                                 by A8,NAT_LAT:def 16;
    take L;
    thus for x being set holds x in the carrier of L iff
     x is MSCongruence of A by A6;
   end;
   uniqueness
   proof
    let C1,C2 be strict SubLattice of EqRelLatt the Sorts of A such that
    A28: for x being set holds x in the carrier of C1 iff
      x is MSCongruence of A and
    A29: for x being set holds x in the carrier of C2 iff
      x is MSCongruence of A;
    A30: now let x be set;
       x in the carrier of C2 iff x is MSCongruence of A by A29;
     hence x in the carrier of C1 iff x in the carrier of C2 by A28;
    end;
    then A31: the carrier of C1 = the carrier of C2 by TARSKI:2;
    then A32: the L_meet of C1 = (the L_meet of EqRelLatt the Sorts of A) |
                  [:the carrier of C2,the carrier of C2:] by NAT_LAT:def 16
             .= the L_meet of C2 by NAT_LAT:def 16;
      the L_join of C1 = (the L_join of EqRelLatt the Sorts of A) |
                  [:the carrier of C2,the carrier of C2:] by A31,NAT_LAT:def 16
             .= the L_join of C2 by NAT_LAT:def 16;
    hence C1 = C2 by A30,A32,TARSKI:2;
   end;
  end;

  theorem Th19:
   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 J.i is Relation of (the Sorts of A).i;
    end;
    then reconsider J as ManySortedRelation of the Sorts of A
                                                          by MSUALG_4:def 2;
      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
      A1: i in the carrier of S & J.i = R;
     then J.i = id ((the Sorts of A).i) by MSUALG_3:def 1;
     hence R is Equivalence_Relation of (the Sorts of A).i by A1;
    end;
    then reconsider J as MSEquivalence_Relation-like
                     ManySortedRelation of the Sorts of A by MSUALG_4:def 3;
    reconsider J as ManySortedRelation of A ;
    reconsider J as MSEquivalence-like ManySortedRelation of A
                                                          by MSUALG_4:def 5;
      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
      A2: for n be Nat st n in dom x holds [x.n,y.n] in
        J.((the_arity_of o)/.n);
     A3: dom x = dom (the_arity_of o) by MSUALG_3:6
              .= Seg len (the_arity_of o) by FINSEQ_1:def 3;
     A4: dom y = dom (the_arity_of o) by MSUALG_3:6
              .= Seg len (the_arity_of o) by FINSEQ_1:def 3;
     then reconsider x' = x , y' = y as FinSequence by A3,FINSEQ_1:def 2;
       now let n be Nat such that A5: 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 A2,A5;
      hence x'.n = y'.n by RELAT_1:def 10;
     end;
     then A6: x = y by A3,A4,FINSEQ_1:17;
       the OperSymbols of S <> {} by MSUALG_1:def 5;
     then o in the OperSymbols of S;
     then A7: o in dom (the ResultSort of S) by FUNCT_2:def 1;
       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 10;
     then Den(o,A).x in (the Sorts of A).((the ResultSort of S).o)
                                                            by A7,FUNCT_1:23;
     then A8: Den(o,A).x in (the Sorts of A).(the_result_sort_of o)
                                                          by MSUALG_1:def 7;
       J.(the_result_sort_of o) = id ((the Sorts of A).(the_result_sort_of o))
                                                          by MSUALG_3:def 1;
     hence [Den(o,A).x,Den(o,A).y] in J.(the_result_sort_of o)
                                                         by A6,A8,RELAT_1:def
10;
    end;
    hence thesis by MSUALG_4:def 6;
   end;

  theorem Th20:
   [|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 = [:(the Sorts of A).i,(the Sorts of A).i:] by PRALG_2:def 9;
     hence J.i is Relation of (the Sorts of A).i by RELSET_1:def 1;
    end;
    then reconsider J as ManySortedRelation of the Sorts of A
                                                          by MSUALG_4:def 2;
      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
      A1: i in the carrier of S & J.i = R;
     then J.i = [:(the Sorts of A).i,(the Sorts of A).i:] by PRALG_2:def 9
        .= nabla (the Sorts of A).i by EQREL_1:def 1;
     hence R is Equivalence_Relation of (the Sorts of A).i by A1;
    end;
    then reconsider J as MSEquivalence_Relation-like
                     ManySortedRelation of the Sorts of A by MSUALG_4:def 3;
    reconsider J as ManySortedRelation of A ;
    reconsider J as MSEquivalence-like ManySortedRelation of A
                                                          by MSUALG_4:def 5;
      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);
       the OperSymbols of S <> {} by MSUALG_1:def 5;
     then o in the OperSymbols of S;
     then A2: o in dom (the ResultSort of S) by FUNCT_2:def 1;
       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 10;
     then Den(o,A).x in (the Sorts of A).((the ResultSort of S).o)
                                                            by A2,FUNCT_1:23;
     then A3: Den(o,A).x in (the Sorts of A).(the_result_sort_of o)
                                                          by MSUALG_1:def 7;
       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 10;
     then Den(o,A).y in (the Sorts of A).((the ResultSort of S).o)
                                                            by A2,FUNCT_1:23;
     then A4: Den(o,A).y in (the Sorts of A).(the_result_sort_of o)
                                                          by MSUALG_1:def 7;
       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 PRALG_2:def 9;
     hence [Den(o,A).x,Den(o,A).y] in J.(the_result_sort_of o)
                                                       by A3,A4,ZFMISC_1:106;
    end;
    hence thesis by MSUALG_4:def 6;
   end;

  definition
   let S, A;
   cluster CongrLatt A -> bounded;
   coherence
   proof
      ex c being Element of CongrLatt A st
     for a being Element of CongrLatt A holds
       c"/\"a = c & a"/\"c = c
    proof
     reconsider c' = id (the Sorts of A) as MSCongruence of A by Th19;
     reconsider c = c' as Element of CongrLatt A by Def6;
     take c;
     let a be Element of CongrLatt A;
     reconsider a' = a as MSCongruence of A by Def6;
     A1: the L_meet of CongrLatt A = (the L_meet of EqRelLatt the Sorts of A) |
                    [:the carrier of CongrLatt A,the carrier of CongrLatt A:]
                                                          by NAT_LAT:def 16;
     A2: [c,a] in [:the carrier of CongrLatt A,the carrier of CongrLatt A:]
                                                             by ZFMISC_1:106;
     A3: now let i be set; assume A4: i in the carrier of S;
      then reconsider i' = i as Element of S;
      reconsider a2 = a'.i' as Equivalence_Relation of (the Sorts of A).i;
      thus (c' /\ a').i = c'.i /\ a'.i by A4,PBOOLE:def 8
         .= id ((the Sorts of A).i) /\ a2 by MSUALG_3:def 1
         .= id ((the Sorts of A).i) by EQREL_1:17
         .= c'.i by A4,MSUALG_3:def 1;
     end;
     thus c"/\"a = (the L_meet of CongrLatt A).(c,a) by LATTICES:def 2
       .= (the L_meet of CongrLatt A).[c,a] by BINOP_1:def 1
       .= (the L_meet of EqRelLatt the Sorts of A).[c,a] by A1,A2,FUNCT_1:72
       .= (the L_meet of EqRelLatt the Sorts of A).(c,a) by BINOP_1:def 1
       .= c' /\ a' by Def5
       .= c by A3,PBOOLE:3;
     hence a "/\" c = c;
    end;
    then A5: CongrLatt A is lower-bounded by LATTICES:def 13;
      ex c being Element of CongrLatt A st
     for a being Element of CongrLatt A holds
      c"\/"a = c & a"\/"c = c
    proof
     reconsider c' = [|the Sorts of A,the Sorts of A|] as MSCongruence of A
       by Th20;
     reconsider c = c' as Element of CongrLatt A by Def6;
     take c;
     let a be Element of CongrLatt A;
     reconsider a' = a as MSCongruence of A by Def6;
     A6: the L_join of CongrLatt A = (the L_join of EqRelLatt the Sorts of A) |
                   [:the carrier of CongrLatt A,the carrier of CongrLatt A:]
                                                          by NAT_LAT:def 16;
     A7: [c,a] in [:the carrier of CongrLatt A,the carrier of CongrLatt A:]
                                                             by ZFMISC_1:106;
     A8: now let i be set; assume A9: i in the carrier of S;
      then reconsider i' = i as Element of S;
      consider K1 be ManySortedRelation of the Sorts of A such that
       A10: K1 = c' \/ a' & c' "\/" a' = EqCl K1 by Def4;
      reconsider K2 = c'.i' , a2 = a'.i' as
                                  Equivalence_Relation of (the Sorts of A).i;
        (c' \/ a').i = c'.i \/ a'.i by A9,PBOOLE:def 7
           .= [:(the Sorts of A).i,(the Sorts of A).i:] \/ a'.i
                                                         by A9,PRALG_2:def 9
           .= nabla (the Sorts of A).i \/ a2 by EQREL_1:def 1
           .= nabla (the Sorts of A).i by Th4
           .= [:(the Sorts of A).i,(the Sorts of A).i:] by EQREL_1:def 1
           .= c'.i by A9,PRALG_2:def 9;
      hence (c' "\/" a').i = EqCl K2 by A10,Def3
         .= c'.i by Th3;
     end;
     thus c"\/"a = (the L_join of CongrLatt A).(c,a) by LATTICES:def 1
           .= (the L_join of CongrLatt A).[c,a] by BINOP_1:def 1
           .= (the L_join of EqRelLatt the Sorts of A).[c,a]
                                                        by A6,A7,FUNCT_1:72
           .= (the L_join of EqRelLatt the Sorts of A).(c,a) by BINOP_1:def 1
           .= c' "\/" a' by Def5
           .= c by A8,PBOOLE:3;
      hence a"\/"c = c;
    end;
    then CongrLatt A is upper-bounded by LATTICES:def 14;
    hence CongrLatt A is bounded by A5,LATTICES:def 15;
   end;
  end;

  theorem
     Bottom CongrLatt A = id (the Sorts of A)
   proof
    set K = id (the Sorts of A);
      K is MSCongruence of A by Th19;
    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,the carrier of CongrLatt A:]
                                                          by NAT_LAT:def 16;
      now let a be Element of CongrLatt A;
     reconsider K' = K , a' = 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:106;
     A3: now let i be set; assume A4: i in the carrier of S;
      then reconsider i' = i as Element of S;
      reconsider a2 = a'.i' as
               Equivalence_Relation of (the Sorts of A).i by MSUALG_4:def 3;
      thus (K' /\ a').i = K'.i /\ a'.i by A4,PBOOLE:def 8
         .= id ((the Sorts of A).i) /\ a2 by MSUALG_3:def 1
         .= id ((the Sorts of A).i) by EQREL_1:17
         .= K'.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 CongrLatt A).[K,a] by BINOP_1:def 1
       .= (the L_meet of EqRelLatt the Sorts of A).[K,a] by A1,A2,FUNCT_1:72
       .= (the L_meet of EqRelLatt the Sorts of A).(K,a) by BINOP_1:def 1
       .= K' /\ a' by Def5
       .= K by A3,PBOOLE:3;
     hence a "/\" K = K;
    end;
    hence thesis by LATTICES:def 16;
   end;

  theorem
     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 Th20;
    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,the carrier of CongrLatt A:]
                                                          by NAT_LAT:def 16;
  now let a be Element of CongrLatt A;
     reconsider K' = K , a' = 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:106;
     A3: now let i be set; assume A4: i in the carrier of S;
      then reconsider i' = i as Element of S;
      consider K1 be ManySortedRelation of the Sorts of A such that
       A5: K1 = K' \/ a' & K' "\/" a' = EqCl K1 by Def4;
      reconsider K2 = K'.i' , a2 = a'.i' as
               Equivalence_Relation of (the Sorts of A).i by MSUALG_4:def 3;
        (K' \/ a').i = K'.i \/ a'.i by A4,PBOOLE:def 7
           .= [:(the Sorts of A).i,(the Sorts of A).i:] \/ a'.i
                                                         by A4,PRALG_2:def 9
           .= nabla (the Sorts of A).i \/ a2 by EQREL_1:def 1
           .= nabla (the Sorts of A).i by Th4
           .= [:(the Sorts of A).i,(the Sorts of A).i:] by EQREL_1:def 1
           .= K'.i by A4,PRALG_2:def 9;
      hence (K' "\/" a').i = EqCl K2 by A5,Def3
         .= K'.i by Th3;
     end;
     thus K "\/" a = (the L_join of CongrLatt A).(K,a) by LATTICES:def 1
       .= (the L_join of CongrLatt A).[K,a] by BINOP_1:def 1
       .= (the L_join of EqRelLatt the Sorts of A).[K,a] by A1,A2,FUNCT_1:72
       .= (the L_join of EqRelLatt the Sorts of A).(K,a) by BINOP_1:def 1
       .= K' "\/" a' by Def5
       .= K by A3,PBOOLE:3;
     hence a "\/" K = K;
    end;
    hence thesis by LATTICES:def 17;
   end;


Back to top