msualg_8.miz



    begin

    reserve I for non empty set;

    reserve M for ManySortedSet of I;

    reserve Y,x,y,y1,i,j for set;

    reserve k for Element of NAT ;

    reserve p for FinSequence;

    reserve S for non void non empty ManySortedSign;

    reserve A for non-empty MSAlgebra over S;

    theorem :: MSUALG_8:1

    

     Th1: for n be Nat, p be FinSequence holds 1 <= n & n < ( len p) iff n in ( dom p) & (n + 1) in ( dom p)

    proof

      let n be Nat;

      let p be FinSequence;

      thus 1 <= n & n < ( len p) implies n in ( dom p) & (n + 1) in ( dom p)

      proof

        assume that

         A1: 1 <= n and

         A2: n < ( len p);

        1 <= (n + 1) & (n + 1) <= ( len p) by A2, NAT_1: 11, NAT_1: 13;

        then

         A3: (n + 1) in ( Seg ( len p)) by FINSEQ_1: 1;

        n in ( Seg ( len p)) by A1, A2, FINSEQ_1: 1;

        hence thesis by A3, FINSEQ_1:def 3;

      end;

      thus n in ( dom p) & (n + 1) in ( dom p) implies 1 <= n & n < ( len p)

      proof

        assume that

         A4: n in ( dom p) and

         A5: (n + 1) in ( dom p);

        (n + 1) in ( Seg ( len p)) by A5, FINSEQ_1:def 3;

        then

         A6: (n + 1) <= ( len p) by FINSEQ_1: 1;

        n in ( Seg ( len p)) by A4, FINSEQ_1:def 3;

        hence thesis by A6, FINSEQ_1: 1, NAT_1: 13;

      end;

    end;

    scheme :: MSUALG_8:sch1

    NonUniqSeqEx { A() -> Element of NAT , P[ object, object] } :

ex p st ( dom p) = ( Seg A()) & for k st k in ( Seg A()) holds P[k, (p . k)]

      provided

       A1: for k st k in ( Seg A()) holds ex x be object st P[k, x];

      

       A2: for x be object st x in ( Seg A()) holds ex y be object st P[x, y] by A1;

      consider f be Function such that

       A3: ( dom f) = ( Seg A()) & for x be object st x in ( Seg A()) holds P[x, (f . x)] from CLASSES1:sch 1( A2);

      reconsider p = f as FinSequence by A3, FINSEQ_1:def 2;

      take p;

      thus thesis by A3;

    end;

    theorem :: MSUALG_8:2

    

     Th2: for a,b be Element of ( EqRelLatt Y) holds for A,B be Equivalence_Relation of Y st a = A & b = B holds a [= b iff A c= B

    proof

      let a,b be Element of ( EqRelLatt Y);

      let A,B be Equivalence_Relation of Y;

      assume that

       A1: a = A and

       A2: b = B;

      thus a [= b implies A c= B

      proof

        assume

         A3: a [= b;

        (A /\ B) = (the L_meet of ( EqRelLatt Y) . (A,B)) by MSUALG_5:def 2

        .= (a "/\" b) by A1, A2, LATTICES:def 2

        .= A by A1, A3, LATTICES: 4;

        hence thesis by XBOOLE_1: 17;

      end;

      thus A c= B implies a [= b

      proof

        assume

         A4: A c= B;

        (a "/\" b) = (the L_meet of ( EqRelLatt Y) . (A,B)) by A1, A2, LATTICES:def 2

        .= (A /\ B) by MSUALG_5:def 2

        .= a by A1, A4, XBOOLE_1: 28;

        hence thesis by LATTICES: 4;

      end;

    end;

    registration

      let Y;

      cluster ( EqRelLatt Y) -> bounded;

      coherence

      proof

        ex c be Element of ( EqRelLatt Y) st for a be Element of ( EqRelLatt Y) holds (c "\/" a) = c & (a "\/" c) = c

        proof

          set c9 = ( nabla Y);

          reconsider c = c9 as Element of ( EqRelLatt Y) by MSUALG_5: 21;

          take c;

          let a be Element of ( EqRelLatt Y);

          reconsider a9 = a as Equivalence_Relation of Y by MSUALG_5: 21;

          

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

          .= (c9 "\/" a9) by MSUALG_5:def 2

          .= ( EqCl (c9 \/ a9)) by MSUALG_5: 1

          .= ( EqCl c9) by EQREL_1: 1

          .= c by MSUALG_5: 2;

          hence thesis;

        end;

        then

         A1: ( EqRelLatt Y) is upper-bounded by LATTICES:def 14;

        ex c be Element of ( EqRelLatt Y) st for a be Element of ( EqRelLatt Y) holds (c "/\" a) = c & (a "/\" c) = c

        proof

          set c9 = ( id Y);

          reconsider c = c9 as Element of ( EqRelLatt Y) by MSUALG_5: 21;

          take c;

          let a be Element of ( EqRelLatt Y);

          reconsider a9 = a as Equivalence_Relation of Y by MSUALG_5: 21;

          

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

          .= (c9 /\ a9) by MSUALG_5:def 2

          .= c by EQREL_1: 10;

          hence thesis;

        end;

        then ( EqRelLatt Y) is lower-bounded by LATTICES:def 13;

        hence thesis by A1;

      end;

    end

    theorem :: MSUALG_8:3

    ( Bottom ( EqRelLatt Y)) = ( id Y)

    proof

      reconsider K = ( id Y) as Element of ( EqRelLatt Y) by MSUALG_5: 21;

      now

        let a be Element of ( EqRelLatt Y);

        reconsider a9 = a as Equivalence_Relation of Y by MSUALG_5: 21;

        

        thus (K "/\" a) = (the L_meet of ( EqRelLatt Y) . (K,a)) by LATTICES:def 2

        .= (( id Y) /\ a9) by MSUALG_5:def 2

        .= K by EQREL_1: 10;

        hence (a "/\" K) = K;

      end;

      hence thesis by LATTICES:def 16;

    end;

    theorem :: MSUALG_8:4

    ( Top ( EqRelLatt Y)) = ( nabla Y)

    proof

      reconsider K = ( nabla Y) as Element of ( EqRelLatt Y) by MSUALG_5: 21;

      now

        let a be Element of ( EqRelLatt Y);

        reconsider a9 = a as Equivalence_Relation of Y by MSUALG_5: 21;

        

        thus (K "\/" a) = (the L_join of ( EqRelLatt Y) . (K,a)) by LATTICES:def 1

        .= (( nabla Y) "\/" a9) by MSUALG_5:def 2

        .= ( EqCl (( nabla Y) \/ a9)) by MSUALG_5: 1

        .= ( EqCl ( nabla Y)) by EQREL_1: 1

        .= K by MSUALG_5: 2;

        hence (a "\/" K) = K;

      end;

      hence thesis by LATTICES:def 17;

    end;

    theorem :: MSUALG_8:5

    

     Th5: ( EqRelLatt Y) is complete

    proof

      for X be Subset of ( EqRelLatt Y) holds ex a be Element of ( EqRelLatt Y) st a is_less_than X & for b be Element of ( EqRelLatt Y) st b is_less_than X holds b [= a

      proof

        let X be Subset of ( EqRelLatt Y);

        per cases ;

          suppose

           A1: X is empty;

          take a = ( Top ( EqRelLatt Y));

          for q be Element of ( EqRelLatt Y) st q in X holds a [= q by A1;

          hence a is_less_than X by LATTICE3:def 16;

          let b be Element of ( EqRelLatt Y);

          assume b is_less_than X;

          thus thesis by LATTICES: 19;

        end;

          suppose

           A2: X is non empty;

          set a = ( meet X);

          X c= ( bool [:Y, Y:])

          proof

            let x be object;

            assume x in X;

            then x is Equivalence_Relation of Y by MSUALG_5: 21;

            hence thesis;

          end;

          then

          reconsider X9 = X as Subset-Family of [:Y, Y:];

          for Z be set st Z in X holds Z is Equivalence_Relation of Y by MSUALG_5: 21;

          then ( meet X9) is Equivalence_Relation of Y by A2, EQREL_1: 11;

          then

          reconsider a as Equivalence_Relation of Y;

          set a9 = a;

          reconsider a as Element of ( EqRelLatt Y) by MSUALG_5: 21;

          take a;

          now

            let q be Element of ( EqRelLatt Y);

            reconsider q9 = q as Equivalence_Relation of Y by MSUALG_5: 21;

            assume q in X;

            then a9 c= q9 by SETFAM_1: 3;

            hence a [= q by Th2;

          end;

          hence a is_less_than X by LATTICE3:def 16;

          now

            let b be Element of ( EqRelLatt Y);

            reconsider b9 = b as Equivalence_Relation of Y by MSUALG_5: 21;

            assume

             A3: b is_less_than X;

            now

              let x be object;

              assume

               A4: x in b9;

              now

                let Z be set;

                assume

                 A5: Z in X;

                then

                reconsider Z1 = Z as Element of ( EqRelLatt Y);

                reconsider Z9 = Z1 as Equivalence_Relation of Y by MSUALG_5: 21;

                b [= Z1 by A3, A5, LATTICE3:def 16;

                then b9 c= Z9 by Th2;

                hence x in Z by A4;

              end;

              hence x in ( meet X) by A2, SETFAM_1:def 1;

            end;

            then b9 c= ( meet X);

            hence b [= a by Th2;

          end;

          hence thesis;

        end;

      end;

      hence thesis by VECTSP_8:def 6;

    end;

    registration

      let Y;

      cluster ( EqRelLatt Y) -> complete;

      coherence by Th5;

    end

    theorem :: MSUALG_8:6

    

     Th6: for Y be set holds for X be Subset of ( EqRelLatt Y) holds ( union X) is Relation of Y

    proof

      let Y be set;

      let X be Subset of ( EqRelLatt Y);

      now

        let x be object;

        assume x in ( union X);

        then

        consider X9 be set such that

         A1: x in X9 and

         A2: X9 in X by TARSKI:def 4;

        X9 is Equivalence_Relation of Y by A2, MSUALG_5: 21;

        hence x in [:Y, Y:] by A1;

      end;

      hence thesis by TARSKI:def 3;

    end;

    theorem :: MSUALG_8:7

    

     Th7: for Y be set holds for X be Subset of ( EqRelLatt Y) holds ( union X) c= ( "\/" X)

    proof

      let Y be set;

      let X be Subset of ( EqRelLatt Y);

      reconsider X9 = ( "\/" X) as Equivalence_Relation of Y by MSUALG_5: 21;

      let x be object;

      assume x in ( union X);

      then

      consider X1 be set such that

       A1: x in X1 and

       A2: X1 in X by TARSKI:def 4;

      reconsider X1 as Element of ( EqRelLatt Y) by A2;

      reconsider X2 = X1 as Equivalence_Relation of Y by MSUALG_5: 21;

      X is_less_than ( "\/" X) by LATTICE3:def 21;

      then X1 [= ( "\/" X) by A2, LATTICE3:def 17;

      then X2 c= X9 by Th2;

      hence thesis by A1;

    end;

    theorem :: MSUALG_8:8

    

     Th8: for Y be set holds for X be Subset of ( EqRelLatt Y) holds for R be Relation of Y st R = ( union X) holds ( "\/" X) = ( EqCl R)

    proof

      let Y be set;

      let X be Subset of ( EqRelLatt Y);

      let R be Relation of Y;

      reconsider X1 = ( "\/" X) as Equivalence_Relation of Y by MSUALG_5: 21;

      assume

       A1: R = ( union X);

       A2:

      now

        let EqR be Equivalence_Relation of Y;

        reconsider EqR1 = EqR as Element of ( EqRelLatt Y) by MSUALG_5: 21;

        assume

         A3: R c= EqR;

        now

          let q be Element of ( EqRelLatt Y);

          reconsider q1 = q as Equivalence_Relation of Y by MSUALG_5: 21;

          assume

           A4: q in X;

          now

            let x be object;

            assume x in q1;

            then x in ( union X) by A4, TARSKI:def 4;

            hence x in EqR by A1, A3;

          end;

          then q1 c= EqR;

          hence q [= EqR1 by Th2;

        end;

        then X is_less_than EqR1 by LATTICE3:def 17;

        then ( "\/" X) [= EqR1 by LATTICE3:def 21;

        hence X1 c= EqR by Th2;

      end;

      R c= ( "\/" X) by A1, Th7;

      hence thesis by A2, MSUALG_5:def 1;

    end;

    theorem :: MSUALG_8:9

    

     Th9: for Y be set holds for X be Subset of ( EqRelLatt Y) holds for R be Relation st R = ( union X) holds R = (R ~ )

    proof

      let Y be set;

      let X be Subset of ( EqRelLatt Y);

      let R be Relation;

      assume

       A1: R = ( union X);

      now

        let x,y be object;

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

        proof

          assume [x, y] in R;

          then

          consider Z be set such that

           A2: [x, y] in Z and

           A3: Z in X by A1, TARSKI:def 4;

          reconsider Z as Equivalence_Relation of Y by A3, MSUALG_5: 21;

           [y, x] in Z by A2, EQREL_1: 6;

          then [y, x] in R by A1, A3, TARSKI:def 4;

          hence thesis by RELAT_1:def 7;

        end;

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

        proof

          assume [x, y] in (R ~ );

          then [y, x] in R by RELAT_1:def 7;

          then

          consider Z be set such that

           A4: [y, x] in Z and

           A5: Z in X by A1, TARSKI:def 4;

          reconsider Z as Equivalence_Relation of Y by A5, MSUALG_5: 21;

           [x, y] in Z by A4, EQREL_1: 6;

          hence thesis by A1, A5, TARSKI:def 4;

        end;

      end;

      hence thesis by RELAT_1:def 2;

    end;

    theorem :: MSUALG_8:10

    

     Th10: for Y be set holds for X be Subset of ( EqRelLatt Y) holds x in Y & y in Y implies ( [x, y] in ( "\/" X) iff ex f be FinSequence st 1 <= ( len f) & x = (f . 1) & y = (f . ( len f)) & for i be Nat st 1 <= i & i < ( len f) holds [(f . i), (f . (i + 1))] in ( union X))

    proof

      let Y be set;

      let X be Subset of ( EqRelLatt Y);

      assume that

       A1: x in Y and

       A2: y in Y;

      reconsider Y9 = Y as non empty set by A1;

      reconsider x9 = x, y9 = y as Element of Y9 by A1, A2;

      reconsider R = ( union X) as Relation of Y9 by Th6;

      R = (R ~ ) by Th9;

      then

       A3: (R \/ (R ~ )) = R;

      

       A4: [x, y] in ( "\/" X) implies R reduces (x,y)

      proof

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

        then [x9, y9] in ( EqCl R) by Th8;

        then (x,y) are_convertible_wrt R by MSUALG_6: 41;

        hence thesis by A3, REWRITE1:def 4;

      end;

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

      proof

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

        then

        consider f be FinSequence such that

         A5: ( len f) > 0 and

         A6: x = (f . 1) & y = (f . ( len f)) and

         A7: for i be Nat st i in ( dom f) & (i + 1) in ( dom f) holds [(f . i), (f . (i + 1))] in R by A4, REWRITE1: 11;

        take f;

        ( 0 + 1) <= ( len f) by A5, NAT_1: 13;

        hence 1 <= ( len f) & x = (f . 1) & y = (f . ( len f)) by A6;

        let i be Nat;

        assume 1 <= i & i < ( len f);

        then i in ( dom f) & (i + 1) in ( dom f) by Th1;

        hence thesis by A7;

      end;

      

       A8: R reduces (x,y) implies [x, y] in ( "\/" X)

      proof

        assume R reduces (x,y);

        then (x,y) are_convertible_wrt R by REWRITE1: 25;

        then [x9, y9] in ( EqCl R) by MSUALG_6: 41;

        hence thesis by Th8;

      end;

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

      proof

        given f be FinSequence such that

         A9: 1 <= ( len f) and

         A10: x = (f . 1) & y = (f . ( len f)) and

         A11: for i be Nat st 1 <= i & i < ( len f) holds [(f . i), (f . (i + 1))] in ( union X);

         A12:

        now

          let i be Nat;

          assume i in ( dom f) & (i + 1) in ( dom f);

          then 1 <= i & i < ( len f) by Th1;

          hence [(f . i), (f . (i + 1))] in ( union X) by A11;

        end;

        ( 0 + 1) <= ( len f) by A9;

        then ( len f) > 0 by NAT_1: 13;

        hence thesis by A8, A10, A12, REWRITE1: 11;

      end;

    end;

    begin

    theorem :: MSUALG_8:11

    

     Th11: for B be Subset of ( CongrLatt A) holds ( "/\" (B,( EqRelLatt the Sorts of A))) is MSCongruence of A

    proof

      set M = the Sorts of A;

      set E = ( EqRelLatt M);

      set C = ( CongrLatt A);

      let B be Subset of C;

      set d9 = ( "/\" (B,E));

      reconsider d = d9 as Equivalence_Relation of the Sorts of A by MSUALG_5:def 5;

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

      the carrier of C c= the carrier of E by NAT_LAT:def 12;

      then

      reconsider B1 = B as Subset of E by XBOOLE_1: 1;

      reconsider B1 as SubsetFamily of [|M, M|] by MSUALG_7: 5;

      per cases ;

        suppose B is empty;

        then

        reconsider B9 = B as empty Subset of ( CongrLatt A);

        for q be Element of E st q in B9 holds ( Top E) [= q;

        then

         A1: ( Top E) is_less_than B by LATTICE3:def 16;

        for b be Element of E st b is_less_than B holds b [= ( Top E) by LATTICES: 19;

        

        then ( "/\" (B,E)) = ( Top E) by A1, LATTICE3: 34

        .= [|M, M|] by MSUALG_7: 4;

        hence thesis by MSUALG_5: 18;

      end;

        suppose

         A2: B is non empty;

        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 (d . (( the_arity_of o) /. n))) holds [(( Den (o,A)) . x), (( Den (o,A)) . y)] in (d . ( the_result_sort_of o))

        proof

          reconsider B19 = B1 as non empty SubsetFamily of [|M, M|] by A2;

          reconsider m = ( meet |:B1:|) as Equivalence_Relation of M by A2, MSUALG_7: 8;

          let o be OperSymbol of S;

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

          

           A3: |:B19:| is non-empty;

          assume

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

           A5:

          now

            let q be MSCongruence of A;

            assume

             A6: q in B;

            now

              let n be Nat;

              assume n in ( dom x);

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

              then

               A7: [(x . n), (y . n)] in (m . (( the_arity_of o) /. n)) by A2, MSUALG_7: 10;

              m c= q by A6, MSUALG_7: 7;

              then (m . (( the_arity_of o) /. n)) c= (q . (( the_arity_of o) /. n)) by PBOOLE:def 2;

              hence [(x . n), (y . n)] in (q . (( the_arity_of o) /. n)) by A7;

            end;

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

          end;

          

           A8: ( |:B1:| . ( the_result_sort_of o)) = { (x1 . ( the_result_sort_of o)) where x1 be Element of ( Bool [|M, M|]) : x1 in B } by A2, CLOSURE2: 14;

          now

            let Y be set;

            assume Y in ( |:B1:| . ( the_result_sort_of o));

            then

            consider z be Element of ( Bool [|M, M|]) such that

             A9: Y = (z . ( the_result_sort_of o)) and

             A10: z in B by A8;

            reconsider z9 = z as MSCongruence of A by A10, MSUALG_5:def 6;

             [(( Den (o,A)) . x), (( Den (o,A)) . y)] in (z9 . ( the_result_sort_of o)) by A5, A10;

            hence [(( Den (o,A)) . x), (( Den (o,A)) . y)] in Y by A9;

          end;

          then (ex Q be Subset-Family of ( [|M, M|] . ( the_result_sort_of o)) st Q = ( |:B1:| . ( the_result_sort_of o)) & (m . ( the_result_sort_of o)) = ( Intersect Q)) & [(( Den (o,A)) . x), (( Den (o,A)) . y)] in ( meet ( |:B1:| . ( the_result_sort_of o))) by A3, MSSUBFAM:def 1, SETFAM_1:def 1;

          then [(( Den (o,A)) . x), (( Den (o,A)) . y)] in (m . ( the_result_sort_of o)) by A3, SETFAM_1:def 9;

          hence thesis by A2, MSUALG_7: 10;

        end;

        hence thesis by MSUALG_4:def 4;

      end;

    end;

    definition

      let S, A;

      let E be Element of ( EqRelLatt the Sorts of A);

      :: MSUALG_8:def1

      func CongrCl E -> MSCongruence of A equals ( "/\" ({ x where x be Element of ( EqRelLatt the Sorts of A) : x is MSCongruence of A & E [= x },( EqRelLatt the Sorts of A)));

      coherence

      proof

        set Z = { x where x be Element of ( EqRelLatt the Sorts of A) : x is MSCongruence of A & E [= x };

        now

          let z be object;

          assume z in Z;

          then ex z1 be Element of ( EqRelLatt the Sorts of A) st z = z1 & z1 is MSCongruence of A & E [= z1;

          hence z in the carrier of ( CongrLatt A) by MSUALG_5:def 6;

        end;

        then

        reconsider Z9 = Z as Subset of ( CongrLatt A) by TARSKI:def 3;

        ( "/\" (Z9,( EqRelLatt the Sorts of A))) is MSCongruence of A by Th11;

        hence thesis;

      end;

    end

    definition

      let S, A;

      let X be Subset of ( EqRelLatt the Sorts of A);

      :: MSUALG_8:def2

      func CongrCl X -> MSCongruence of A equals ( "/\" ({ x where x be Element of ( EqRelLatt the Sorts of A) : x is MSCongruence of A & X is_less_than x },( EqRelLatt the Sorts of A)));

      coherence

      proof

        set Z = { x where x be Element of ( EqRelLatt the Sorts of A) : x is MSCongruence of A & X is_less_than x };

        now

          let z be object;

          assume z in Z;

          then ex z1 be Element of ( EqRelLatt the Sorts of A) st z = z1 & z1 is MSCongruence of A & X is_less_than z1;

          hence z in the carrier of ( CongrLatt A) by MSUALG_5:def 6;

        end;

        then

        reconsider Z9 = Z as Subset of ( CongrLatt A) by TARSKI:def 3;

        ( "/\" (Z9,( EqRelLatt the Sorts of A))) is MSCongruence of A by Th11;

        hence thesis;

      end;

    end

    theorem :: MSUALG_8:12

    for C be Element of ( EqRelLatt the Sorts of A) st C is MSCongruence of A holds ( CongrCl C) = C

    proof

      let C be Element of ( EqRelLatt the Sorts of A);

      set Z = { x where x be Element of ( EqRelLatt the Sorts of A) : x is MSCongruence of A & C [= x };

      now

        let q be Element of ( EqRelLatt the Sorts of A);

        assume q in Z;

        then ex x be Element of ( EqRelLatt the Sorts of A) st q = x & x is MSCongruence of A & C [= x;

        hence C [= q;

      end;

      then

       A1: C is_less_than Z by LATTICE3:def 16;

      assume C is MSCongruence of A;

      then C in Z;

      hence thesis by A1, LATTICE3: 41;

    end;

    theorem :: MSUALG_8:13

    for X be Subset of ( EqRelLatt the Sorts of A) holds ( CongrCl ( "\/" (X,( EqRelLatt the Sorts of A)))) = ( CongrCl X)

    proof

      let X be Subset of ( EqRelLatt the Sorts of A);

      set D1 = { x where x be Element of ( EqRelLatt the Sorts of A) : x is MSCongruence of A & ( "\/" (X,( EqRelLatt the Sorts of A))) [= x };

      set D2 = { x where x be Element of ( EqRelLatt the Sorts of A) : x is MSCongruence of A & X is_less_than x };

      

       A1: D1 c= D2

      proof

        let x1 be object;

        assume x1 in D1;

        then

        consider x be Element of ( EqRelLatt the Sorts of A) such that

         A2: x1 = x & x is MSCongruence of A and

         A3: ( "\/" (X,( EqRelLatt the Sorts of A))) [= x;

        now

          let q be Element of ( EqRelLatt the Sorts of A);

          

           A4: X is_less_than ( "\/" (X,( EqRelLatt the Sorts of A))) by LATTICE3:def 21;

          assume q in X;

          then q [= ( "\/" (X,( EqRelLatt the Sorts of A))) by A4, LATTICE3:def 17;

          hence q [= x by A3, LATTICES: 7;

        end;

        then X is_less_than x by LATTICE3:def 17;

        hence thesis by A2;

      end;

      D2 c= D1

      proof

        let x1 be object;

        assume x1 in D2;

        then

        consider x be Element of ( EqRelLatt the Sorts of A) such that

         A5: x1 = x & x is MSCongruence of A and

         A6: X is_less_than x;

        ( "\/" (X,( EqRelLatt the Sorts of A))) [= x by A6, LATTICE3:def 21;

        hence thesis by A5;

      end;

      hence thesis by A1, XBOOLE_0:def 10;

    end;

    theorem :: MSUALG_8:14

    for B1,B2 be Subset of ( CongrLatt A), C1,C2 be MSCongruence of A st C1 = ( "\/" (B1,( EqRelLatt the Sorts of A))) & C2 = ( "\/" (B2,( EqRelLatt the Sorts of A))) holds (C1 "\/" C2) = ( "\/" ((B1 \/ B2),( EqRelLatt the Sorts of A)))

    proof

      let B1,B2 be Subset of ( CongrLatt A);

      let C1,C2 be MSCongruence of A;

      set C = ( EqRelLatt the Sorts of A);

      assume

       A1: C1 = ( "\/" (B1,( EqRelLatt the Sorts of A))) & C2 = ( "\/" (B2,( EqRelLatt the Sorts of A)));

      the carrier of ( CongrLatt A) c= the carrier of ( EqRelLatt the Sorts of A) by NAT_LAT:def 12;

      then

      reconsider D1 = B1, D2 = B2 as Subset of ( EqRelLatt the Sorts of A) by XBOOLE_1: 1;

      

       A2: {( "\/" D1), ( "\/" D2)} c= { ( "\/" Y) where Y be Subset of C : Y in {B1, B2} }

      proof

        let x be object;

        assume x in {( "\/" D1), ( "\/" D2)};

        then

         A3: x = ( "\/" D1) or x = ( "\/" D2) by TARSKI:def 2;

        D1 in {B1, B2} & D2 in {B1, B2} by TARSKI:def 2;

        hence thesis by A3;

      end;

      { ( "\/" Y) where Y be Subset of C : Y in {B1, B2} } c= {( "\/" D1), ( "\/" D2)}

      proof

        let x be object;

        assume x in { ( "\/" Y) where Y be Subset of C : Y in {B1, B2} };

        then

        consider X1 be Subset of C such that

         A4: x = ( "\/" X1) and

         A5: X1 in {B1, B2};

        X1 = B1 or X1 = B2 by A5, TARSKI:def 2;

        hence thesis by A4, TARSKI:def 2;

      end;

      then

       A6: { ( "\/" Y) where Y be Subset of C : Y in {B1, B2} } = {( "\/" D1), ( "\/" D2)} by A2;

      now

        let i be object;

        assume i in {B1, B2};

        then i = D1 or i = D2 by TARSKI:def 2;

        hence i in ( bool the carrier of C);

      end;

      then

       A7: {B1, B2} c= ( bool the carrier of C);

      

      thus ( "\/" ((B1 \/ B2),( EqRelLatt the Sorts of A))) = ( "\/" (( union {B1, B2}),C)) by ZFMISC_1: 75

      .= ( "\/" ({ ( "\/" Y) where Y be Subset of C : Y in {B1, B2} },C)) by A7, LATTICE3: 48

      .= (( "\/" D1) "\/" ( "\/" D2)) by A6, LATTICE3: 43

      .= (the L_join of C . (C1,C2)) by A1, LATTICES:def 1

      .= (C1 "\/" C2) by MSUALG_5:def 5;

    end;

    theorem :: MSUALG_8:15

    for X be Subset of ( CongrLatt A) holds ( "\/" (X,( EqRelLatt the Sorts of A))) = ( "\/" ({ ( "\/" (X0,( EqRelLatt the Sorts of A))) where X0 be Subset of ( EqRelLatt the Sorts of A) : X0 is finite Subset of X },( EqRelLatt the Sorts of A)))

    proof

      let X be Subset of ( CongrLatt A);

      set E = ( EqRelLatt the Sorts of A);

      set X1 = { X0 where X0 be Subset of E : X0 is finite Subset of X };

      set B1 = { ( "\/" Y) where Y be Subset of E : Y in X1 };

      set B2 = { ( "\/" (X0,( EqRelLatt the Sorts of A))) where X0 be Subset of E : X0 is finite Subset of X };

      

       A1: B2 c= B1

      proof

        let x be object;

        assume x in B2;

        then

        consider Y1 be Subset of E such that

         A2: x = ( "\/" Y1) and

         A3: Y1 is finite Subset of X;

        Y1 in X1 by A3;

        hence thesis by A2;

      end;

      

       A4: X c= ( union X1)

      proof

        let x be object;

        assume

         A5: x in X;

        then

        reconsider x9 = x as Element of ( CongrLatt A);

        the carrier of ( CongrLatt A) c= the carrier of E by NAT_LAT:def 12;

        then

        reconsider x9 as Element of E;

         {x9} is finite Subset of X by A5, SUBSET_1: 41;

        then x in {x} & {x9} in X1 by TARSKI:def 1;

        hence thesis by TARSKI:def 4;

      end;

      ( union X1) c= X

      proof

        let x be object;

        assume x in ( union X1);

        then

        consider Y1 be set such that

         A6: x in Y1 and

         A7: Y1 in X1 by TARSKI:def 4;

        ex Y2 be Subset of E st Y1 = Y2 & Y2 is finite Subset of X by A7;

        hence thesis by A6;

      end;

      then

       A8: X = ( union X1) by A4;

      now

        let i be object;

        assume i in X1;

        then ex I1 be Subset of E st i = I1 & I1 is finite Subset of X;

        hence i in ( bool the carrier of E);

      end;

      then

       A9: X1 c= ( bool the carrier of E);

      B1 c= B2

      proof

        let x be object;

        assume x in B1;

        then

        consider Y1 be Subset of E such that

         A10: x = ( "\/" Y1) and

         A11: Y1 in X1;

        ex Y2 be Subset of E st Y1 = Y2 & Y2 is finite Subset of X by A11;

        hence thesis by A10;

      end;

      then B1 = B2 by A1;

      hence thesis by A9, A8, LATTICE3: 48;

    end;

    theorem :: MSUALG_8:16

    

     Th16: for i be Element of I holds for e be Equivalence_Relation of (M . i) holds ex E be Equivalence_Relation of M st (E . i) = e & for j be Element of I st j <> i holds (E . j) = ( nabla (M . j))

    proof

      let i be Element of I;

      let e be Equivalence_Relation of (M . i);

      defpred C[ object] means $1 = i;

      deffunc F( object) = e;

      deffunc G( object) = ( nabla (M . $1));

      consider E be Function such that

       A1: ( dom E) = I and

       A2: for j be object st j in I holds ( C[j] implies (E . j) = F(j)) & ( not C[j] implies (E . j) = G(j)) from PARTFUN1:sch 1;

      reconsider E as ManySortedSet of I by A1, PARTFUN1:def 2, RELAT_1:def 18;

      now

        let k be set;

        assume

         A3: k in I;

        per cases ;

          suppose k = i;

          hence (E . k) is Relation of (M . k) by A2;

        end;

          suppose k <> i;

          then (E . k) = ( nabla (M . k)) by A2, A3;

          hence (E . k) is Relation of (M . k);

        end;

      end;

      then

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

      now

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

        assume that

         A4: k in I and

         A5: (E . k) = R;

        per cases ;

          suppose k = i;

          hence R is Equivalence_Relation of (M . k) by A2, A5;

        end;

          suppose k <> i;

          then (E . k) = ( nabla (M . k)) by A2, A4;

          hence R is Equivalence_Relation of (M . k) by A5;

        end;

      end;

      then

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

      take E;

      thus (E . i) = e by A2;

      let j be Element of I;

      assume j <> i;

      hence thesis by A2;

    end;

    notation

      let I be non empty set;

      let M be ManySortedSet of I;

      let i be Element of I;

      let X be Subset of ( EqRelLatt M);

      synonym EqRelSet (X,i) for pi (X,i);

    end

    definition

      let I be non empty set;

      let M be ManySortedSet of I;

      let i be Element of I;

      let X be Subset of ( EqRelLatt M);

      :: original: EqRelSet

      redefine

      :: MSUALG_8:def3

      func EqRelSet (X,i) -> Subset of ( EqRelLatt (M . i)) means

      : Def3: x in it iff ex Eq be Equivalence_Relation of M st x = (Eq . i) & Eq in X;

      coherence

      proof

        ( pi (X,i)) c= the carrier of ( EqRelLatt (M . i))

        proof

          let z be object;

          assume z in ( pi (X,i));

          then

          consider f be Function such that

           A1: f in X and

           A2: z = (f . i) by CARD_3:def 6;

          reconsider f as Equivalence_Relation of M by A1, MSUALG_5:def 5;

          (f . i) is Equivalence_Relation of (M . i) by MSUALG_4:def 2;

          hence thesis by A2, MSUALG_5: 21;

        end;

        hence thesis;

      end;

      compatibility

      proof

        thus for Y be Subset of ( EqRelLatt (M . i)) holds Y = ( pi (X,i)) iff for x holds x in Y iff ex Eq be Equivalence_Relation of M st x = (Eq . i) & Eq in X

        proof

          let Y be Subset of ( EqRelLatt (M . i));

          thus Y = ( pi (X,i)) implies for x holds x in Y iff ex Eq be Equivalence_Relation of M st x = (Eq . i) & Eq in X

          proof

            assume

             A3: Y = ( pi (X,i));

            let x;

            thus x in Y implies ex Eq be Equivalence_Relation of M st x = (Eq . i) & Eq in X

            proof

              assume x in Y;

              then

              consider f be Function such that

               A4: f in X and

               A5: x = (f . i) by A3, CARD_3:def 6;

              reconsider f as Equivalence_Relation of M by A4, MSUALG_5:def 5;

              take f;

              thus thesis by A4, A5;

            end;

            thus thesis by A3, CARD_3:def 6;

          end;

          thus (for x holds x in Y iff ex Eq be Equivalence_Relation of M st x = (Eq . i) & Eq in X) implies Y = ( pi (X,i))

          proof

            assume

             A6: for x holds x in Y iff ex Eq be Equivalence_Relation of M st x = (Eq . i) & Eq in X;

            thus Y c= ( pi (X,i))

            proof

              let y1 be object;

              assume y1 in Y;

              then ex Eq be Equivalence_Relation of M st y1 = (Eq . i) & Eq in X by A6;

              hence thesis by CARD_3:def 6;

            end;

            thus ( pi (X,i)) c= Y

            proof

              let y1 be object;

              assume y1 in ( pi (X,i));

              then

              consider f be Function such that

               A7: f in X and

               A8: y1 = (f . i) by CARD_3:def 6;

              reconsider f as Equivalence_Relation of M by A7, MSUALG_5:def 5;

              ex Eq be Equivalence_Relation of M st y1 = (Eq . i) & Eq in X

              proof

                take f;

                thus thesis by A7, A8;

              end;

              hence thesis by A6;

            end;

          end;

        end;

      end;

    end

    theorem :: MSUALG_8:17

    

     Th17: for i be Element of S holds for X be Subset of ( EqRelLatt the Sorts of A) holds for B be Equivalence_Relation of the Sorts of A st B = ( "\/" X) holds (B . i) = ( "\/" (( EqRelSet (X,i)),( EqRelLatt (the Sorts of A . i))))

    proof

      let i be Element of S;

      set M = the Sorts of A;

      set E = ( EqRelLatt M);

      set Ei = ( EqRelLatt (M . i));

      let X be Subset of E;

      let B be Equivalence_Relation of M;

      reconsider B9 = B as Element of E by MSUALG_5:def 5;

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

      reconsider Bi9 = Bi as Element of Ei by MSUALG_5: 21;

      assume

       A1: B = ( "\/" X);

       A2:

      now

        let ri be Element of Ei;

        reconsider ri9 = ri as Equivalence_Relation of (M . i) by MSUALG_5: 21;

        consider r9 be Equivalence_Relation of the Sorts of A such that

         A3: (r9 . i) = ri9 and

         A4: for j be SortSymbol of S st j <> i holds (r9 . j) = ( nabla (the Sorts of A . j)) by Th16;

        reconsider r = r9 as Element of E by MSUALG_5:def 5;

        assume

         A5: ( EqRelSet (X,i)) is_less_than ri;

        now

          let c be Element of E;

          reconsider c9 = c as Equivalence_Relation of M by MSUALG_5:def 5;

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

          reconsider ci = ci9 as Element of Ei by MSUALG_5: 21;

          assume c in X;

          then ci in ( EqRelSet (X,i)) by Def3;

          then

           A6: ci [= ri by A5, LATTICE3:def 17;

          now

            let j be object;

            assume

             A7: j in the carrier of S;

            then

            reconsider j9 = j as Element of S;

            reconsider rj9 = (r9 . j9), cj9 = (c9 . j9) as Equivalence_Relation of (M . j) by MSUALG_4:def 2;

            per cases ;

              suppose j = i;

              hence (c9 . j) c= (r9 . j) by A3, A6, Th2;

            end;

              suppose j <> i;

              then (r9 . j) = ( nabla (the Sorts of A . j)) by A4, A7;

              then (cj9 /\ rj9) = cj9 by XBOOLE_1: 28;

              hence (c9 . j) c= (r9 . j) by XBOOLE_1: 17;

            end;

          end;

          then c9 c= r9 by PBOOLE:def 2;

          hence c [= r by MSUALG_7: 6;

        end;

        then X is_less_than r by LATTICE3:def 17;

        then B9 [= r by A1, LATTICE3:def 21;

        then B c= r9 by MSUALG_7: 6;

        then Bi c= ri9 by A3, PBOOLE:def 2;

        hence Bi9 [= ri by Th2;

      end;

      now

        let q9 be Element of Ei;

        reconsider q = q9 as Equivalence_Relation of (M . i) by MSUALG_5: 21;

        assume q9 in ( EqRelSet (X,i));

        then

        consider Eq be Equivalence_Relation of M such that

         A8: q9 = (Eq . i) and

         A9: Eq in X by Def3;

        reconsider Eq9 = Eq as Element of E by MSUALG_5:def 5;

        Eq9 [= B9 by A1, A9, LATTICE3: 38;

        then Eq c= B by MSUALG_7: 6;

        then q c= Bi by A8, PBOOLE:def 2;

        hence q9 [= Bi9 by Th2;

      end;

      then ( EqRelSet (X,i)) is_less_than Bi9 by LATTICE3:def 17;

      hence thesis by A2, LATTICE3:def 21;

    end;

    theorem :: MSUALG_8:18

    

     Th18: for X be Subset of ( CongrLatt A) holds ( "\/" (X,( EqRelLatt the Sorts of A))) is MSCongruence of A

    proof

      let X9 be Subset of ( CongrLatt A);

      set M = the Sorts of A;

      set E = ( EqRelLatt M);

      the carrier of ( CongrLatt A) c= the carrier of ( EqRelLatt M) by NAT_LAT:def 12;

      then

      reconsider X = X9 as Subset of ( EqRelLatt M) by XBOOLE_1: 1;

      reconsider V = ( "\/" (X,E)) as Equivalence_Relation of M by MSUALG_5:def 5;

      reconsider V as ManySortedRelation of A;

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

      for s1,s2 be SortSymbol of S holds for t be Function st t is_e.translation_of (A,s1,s2) holds for a,b be set st [a, b] in (V . s1) holds [(t . a), (t . b)] in (V . s2)

      proof

        let s1,s2 be SortSymbol of S;

        let t be Function;

        assume

         A1: t is_e.translation_of (A,s1,s2);

        then

        reconsider t9 = t as Function of (M . s1), (M . s2) by MSUALG_6: 11;

        let a,b be set;

        assume

         A2: [a, b] in (V . s1);

        then

         A3: a in (M . s1) by ZFMISC_1: 87;

        

         A4: b in (M . s1) by A2, ZFMISC_1: 87;

        then

         A5: (t9 . b) in (M . s2) by FUNCT_2: 5;

         [a, b] in ( "\/" ( EqRelSet (X,s1))) by A2, Th17;

        then

        consider f be FinSequence such that

         A6: 1 <= ( len f) and

         A7: a = (f . 1) and

         A8: b = (f . ( len f)) and

         A9: for i be Nat st 1 <= i & i < ( len f) holds [(f . i), (f . (i + 1))] in ( union ( EqRelSet (X,s1))) by A3, A4, Th10;

        

         A10: ex g be FinSequence st 1 <= ( len g) & (t . a) = (g . 1) & (t . b) = (g . ( len g)) & for i be Nat st 1 <= i & i < ( len g) holds [(g . i), (g . (i + 1))] in ( union ( EqRelSet (X,s2)))

        proof

          deffunc F( set) = (t . (f . $1));

          consider g be FinSequence such that

           A11: ( len g) = ( len f) & for k be Nat st k in ( dom g) holds (g . k) = F(k) from FINSEQ_1:sch 2;

          take g;

          thus 1 <= ( len g) by A6, A11;

          

           A12: ( dom g) = ( Seg ( len f)) by A11, FINSEQ_1:def 3;

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

          hence (g . 1) = (t . a) by A7, A11, A12;

          ( len g) in ( Seg ( len f)) by A6, A11, FINSEQ_1: 1;

          hence (g . ( len g)) = (t . b) by A8, A11, A12;

          let j be Nat;

          assume that

           A13: 1 <= j and

           A14: j < ( len g);

          

           A15: 1 <= (j + 1) by A13, NAT_1: 13;

           [(f . j), (f . (j + 1))] in ( union ( EqRelSet (X,s1))) by A9, A11, A13, A14;

          then

          consider Z be set such that

           A16: [(f . j), (f . (j + 1))] in Z and

           A17: Z in ( EqRelSet (X,s1)) by TARSKI:def 4;

          consider Eq be Equivalence_Relation of M such that

           A18: Z = (Eq . s1) and

           A19: Eq in X by A17, Def3;

          reconsider Eq as ManySortedRelation of A;

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

          Eq is MSCongruence of A by A19, MSUALG_5:def 6;

          then

          reconsider Eq as compatible MSEquivalence-like ManySortedRelation of A by MSUALG_6: 27;

          ex W be set st [(t . (f . j)), (t . (f . (j + 1)))] in W & W in ( EqRelSet (X,s2))

          proof

            take W = (Eq . s2);

            thus [(t . (f . j)), (t . (f . (j + 1)))] in W by A1, A16, A18, MSUALG_6:def 8;

            thus thesis by A19, Def3;

          end;

          then

           A20: [(t . (f . j)), (t . (f . (j + 1)))] in ( union ( EqRelSet (X,s2))) by TARSKI:def 4;

          (j + 1) <= ( len f) by A11, A14, NAT_1: 13;

          then

           A21: (j + 1) in ( Seg ( len f)) by A15, FINSEQ_1: 1;

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

          then (g . j) = (t . (f . j)) by A11, A12;

          hence thesis by A11, A12, A20, A21;

        end;

        (t9 . a) in (M . s2) by A3, FUNCT_2: 5;

        then [(t . a), (t . b)] in ( "\/" ( EqRelSet (X,s2))) by A5, A10, Th10;

        hence thesis by Th17;

      end;

      then

      reconsider V as invariant MSEquivalence-like ManySortedRelation of A by MSUALG_6:def 8;

      V is compatible;

      hence thesis by MSUALG_6: 27;

    end;

    theorem :: MSUALG_8:19

    

     Th19: ( CongrLatt A) is /\-inheriting

    proof

      set E = ( EqRelLatt the Sorts of A);

      set C = ( CongrLatt A);

      now

        let B be Subset of C;

        reconsider d = ( "/\" (B,E)) as MSCongruence of A by Th11;

        d in the carrier of C by MSUALG_5:def 6;

        hence ( "/\" (B,E)) in the carrier of C;

      end;

      hence thesis by MSUALG_7:def 2;

    end;

    theorem :: MSUALG_8:20

    

     Th20: ( CongrLatt A) is \/-inheriting

    proof

      set E = ( EqRelLatt the Sorts of A);

      set C = ( CongrLatt A);

      now

        let B be Subset of C;

        reconsider d = ( "\/" (B,E)) as MSCongruence of A by Th18;

        d in the carrier of C by MSUALG_5:def 6;

        hence ( "\/" (B,E)) in the carrier of C;

      end;

      hence thesis by MSUALG_7:def 3;

    end;

    registration

      let S, A;

      cluster ( CongrLatt A) -> /\-inheriting \/-inheriting;

      coherence by Th19, Th20;

    end