msinst_1.miz



    begin

    reserve A for non empty set,

S for non void non empty ManySortedSign;

    reserve x for set;

    definition

      let A;

      :: MSINST_1:def1

      func MSSCat A -> strict non empty AltCatStr means

      : Def1: the carrier of it = ( MSS_set A) & (for i,j be Element of ( MSS_set A) holds (the Arrows of it . (i,j)) = ( MSS_morph (i,j))) & for i,j,k be Object of it st i in ( MSS_set A) & j in ( MSS_set A) & k in ( MSS_set A) holds for f1,f2,g1,g2 be Function st [f1, f2] in (the Arrows of it . (i,j)) & [g1, g2] in (the Arrows of it . (j,k)) holds ((the Comp of it . (i,j,k)) . ( [g1, g2], [f1, f2])) = [(g1 * f1), (g2 * f2)];

      existence

      proof

        set c = ( MSS_set A);

        deffunc F( Element of c, Element of c) = ( MSS_morph ($1,$2));

        consider M be ManySortedSet of [:c, c:] such that

         A1: for i,j be Element of c holds (M . (i,j)) = F(i,j) from ALTCAT_1:sch 2;

        defpred P[ object, object, object] means ex i,j,k be Element of ( MSS_set A) st $3 = [i, j, k] & for f1,f2,g1,g2 be Function st [f1, f2] in (M . (i,j)) & [g1, g2] in (M . (j,k)) & $2 = [ [g1, g2], [f1, f2]] holds $1 = [(g1 * f1), (g2 * f2)];

        

         A2: for ijk be object st ijk in [:c, c, c:] holds for x be object st x in ( {|M, M|} . ijk) holds ex y be object st y in ( {|M|} . ijk) & P[y, x, ijk]

        proof

          let ijk be object;

          assume ijk in [:c, c, c:];

          then

          consider x1,x2,x3 be object such that

           A3: x1 in c & x2 in c & x3 in c and

           A4: ijk = [x1, x2, x3] by MCART_1: 68;

          reconsider x1, x2, x3 as Element of c by A3;

          let x be object;

          

           A5: ( {|M, M|} . (x1,x2,x3)) = ( {|M, M|} . [x1, x2, x3]) & ( {|M, M|} . (x1,x2,x3)) = [:(M . (x2,x3)), (M . (x1,x2)):] by ALTCAT_1:def 4, MULTOP_1:def 1;

          

           A6: ( {|M|} . ijk) = ( {|M|} . (x1,x2,x3)) by A4, MULTOP_1:def 1;

          assume

           A7: x in ( {|M, M|} . ijk);

          then (x `1 ) in (M . (x2,x3)) by A4, A5, MCART_1: 10;

          then (x `1 ) in ( MSS_morph (x2,x3)) by A1;

          then

          consider g1,g2 be Function such that

           A8: (x `1 ) = [g1, g2] and

           A9: (g1,g2) form_morphism_between (x2,x3) by MSALIMIT:def 10;

          (x `2 ) in (M . (x1,x2)) by A4, A7, A5, MCART_1: 10;

          then (x `2 ) in ( MSS_morph (x1,x2)) by A1;

          then

          consider f1,f2 be Function such that

           A10: (x `2 ) = [f1, f2] and

           A11: (f1,f2) form_morphism_between (x1,x2) by MSALIMIT:def 10;

          take y = [(g1 * f1), (g2 * f2)];

          ((g1 * f1),(g2 * f2)) form_morphism_between (x1,x3) by A11, A9, PUA2MSS1: 29;

          then ( {|M|} . (x1,x2,x3)) = (M . (x1,x3)) & y in ( MSS_morph (x1,x3)) by ALTCAT_1:def 3, MSALIMIT:def 10;

          hence y in ( {|M|} . ijk) by A1, A6;

          take x1, x2, x3;

          thus ijk = [x1, x2, x3] by A4;

          let F1,F2,G1,G2 be Function;

          assume that [F1, F2] in (M . (x1,x2)) and [G1, G2] in (M . (x2,x3)) and

           A12: x = [ [G1, G2], [F1, F2]];

          (x `1 ) = [G1, G2] by A12;

          then

           A13: G1 = g1 & G2 = g2 by A8, XTUPLE_0: 1;

          

           A14: (x `2 ) = [F1, F2] by A12;

          then F1 = f1 by A10, XTUPLE_0: 1;

          hence thesis by A10, A14, A13, XTUPLE_0: 1;

        end;

        consider F be ManySortedFunction of {|M, M|}, {|M|} such that

         A15: for ijk be object st ijk in [:c, c, c:] holds ex f be Function of ( {|M, M|} . ijk), ( {|M|} . ijk) st f = (F . ijk) & for x be object st x in ( {|M, M|} . ijk) holds P[(f . x), x, ijk] from MSSUBFAM:sch 1( A2);

        take EX = AltCatStr (# c, M, F #);

        reconsider EX as non empty AltCatStr;

        for i,j,k be Object of EX st i in ( MSS_set A) & j in ( MSS_set A) & k in ( MSS_set A) holds for f1,f2,g1,g2 be Function st [f1, f2] in (the Arrows of EX . (i,j)) & [g1, g2] in (the Arrows of EX . (j,k)) holds ((the Comp of EX . (i,j,k)) . ( [g1, g2], [f1, f2])) = [(g1 * f1), (g2 * f2)]

        proof

          let i,j,k be Object of EX;

          assume that i in ( MSS_set A) and j in ( MSS_set A) and k in ( MSS_set A);

          let f1,f2,g1,g2 be Function;

          assume

           A16: [f1, f2] in (the Arrows of EX . (i,j)) & [g1, g2] in (the Arrows of EX . (j,k));

          set x = [ [g1, g2], [f1, f2]];

          set ijk = [i, j, k];

          ijk in [:c, c, c:] by MCART_1: 69;

          then

          consider f be Function of ( {|M, M|} . ijk), ( {|M|} . ijk) such that

           A17: f = (F . ijk) and

           A18: for x be object st x in ( {|M, M|} . ijk) holds P[(f . x), x, ijk] by A15;

          

           A19: f = (the Comp of EX . (i,j,k)) by A17, MULTOP_1:def 1;

          ( {|M, M|} . (i,j,k)) = ( {|M, M|} . [i, j, k]) & ( {|M, M|} . (i,j,k)) = [:(M . (j,k)), (M . (i,j)):] by ALTCAT_1:def 4, MULTOP_1:def 1;

          then x in ( {|M, M|} . ijk) by A16, ZFMISC_1: 87;

          then

          consider I,J,K be Element of ( MSS_set A) such that

           A20: ijk = [I, J, K] and

           A21: for f1,f2,g1,g2 be Function st [f1, f2] in (M . (I,J)) & [g1, g2] in (M . (J,K)) & x = [ [g1, g2], [f1, f2]] holds (f . x) = [(g1 * f1), (g2 * f2)] by A18;

          

           A22: K = k by A20, XTUPLE_0: 3;

          I = i & J = j by A20, XTUPLE_0: 3;

          hence thesis by A16, A21, A22, A19;

        end;

        hence thesis by A1;

      end;

      uniqueness

      proof

        set c = ( MSS_set A);

        let A1,A2 be non empty strict AltCatStr such that

         A23: the carrier of A1 = ( MSS_set A) and

         A24: for i,j be Element of ( MSS_set A) holds (the Arrows of A1 . (i,j)) = ( MSS_morph (i,j)) and

         A25: for i,j,k be Object of A1 st i in ( MSS_set A) & j in ( MSS_set A) & k in ( MSS_set A) holds for f1,f2,g1,g2 be Function st [f1, f2] in (the Arrows of A1 . (i,j)) & [g1, g2] in (the Arrows of A1 . (j,k)) holds ((the Comp of A1 . (i,j,k)) . ( [g1, g2], [f1, f2])) = [(g1 * f1), (g2 * f2)] and

         A26: the carrier of A2 = ( MSS_set A) and

         A27: for i,j be Element of ( MSS_set A) holds (the Arrows of A2 . (i,j)) = ( MSS_morph (i,j)) and

         A28: for i,j,k be Object of A2 st i in ( MSS_set A) & j in ( MSS_set A) & k in ( MSS_set A) holds for f1,f2,g1,g2 be Function st [f1, f2] in (the Arrows of A2 . (i,j)) & [g1, g2] in (the Arrows of A2 . (j,k)) holds ((the Comp of A2 . (i,j,k)) . ( [g1, g2], [f1, f2])) = [(g1 * f1), (g2 * f2)];

        reconsider AA2 = the Arrows of A2 as ManySortedSet of [:c, c:] by A26;

        reconsider AA1 = the Arrows of A1 as ManySortedSet of [:c, c:] by A23;

        reconsider CC1 = the Comp of A1, CC2 = the Comp of A2 as ManySortedSet of [:c, c, c:] by A23, A26;

         A29:

        now

          let i,j be Element of ( MSS_set A);

          

          thus (AA1 . (i,j)) = ( MSS_morph (i,j)) by A24

          .= (AA2 . (i,j)) by A27;

        end;

        then

         A30: AA1 = AA2 by ALTCAT_1: 7;

        now

          let i,j,k be object;

          set ijk = [i, j, k];

          

           A31: (CC1 . (i,j,k)) = (CC1 . [i, j, k]) by MULTOP_1:def 1;

          assume

           A32: i in ( MSS_set A) & j in ( MSS_set A) & k in ( MSS_set A);

          then

          reconsider i9 = i, j9 = j, k9 = k as Element of c;

          reconsider I9 = i, J9 = j, K9 = k as Element of A2 by A26, A32;

          reconsider I = i, J = j, K = k as Element of A1 by A23, A32;

          

           A33: ijk in [:c, c, c:] by A32, MCART_1: 69;

          

           A34: (CC2 . (i,j,k)) = (CC2 . [i, j, k]) by MULTOP_1:def 1;

          thus (CC1 . (i,j,k)) = (CC2 . (i,j,k))

          proof

            reconsider Cj = (CC2 . ijk) as Function of ( {|AA2, AA2|} . ijk), ( {|AA2|} . ijk) by A26, A33, PBOOLE:def 15;

            reconsider Ci = (CC1 . ijk) as Function of ( {|AA1, AA1|} . ijk), ( {|AA1|} . ijk) by A23, A33, PBOOLE:def 15;

            per cases ;

              suppose

               A35: ( {|AA1|} . ijk) <> {} ;

              

               A36: for x be object st x in ( {|AA1, AA1|} . ijk) holds (Ci . x) = (Cj . x)

              proof

                let x be object;

                assume

                 A37: x in ( {|AA1, AA1|} . ijk);

                then x in ( {|AA1, AA1|} . (i,j,k)) by MULTOP_1:def 1;

                then

                 A38: x in [:(AA1 . (j,k)), (AA1 . (i,j)):] by A32, ALTCAT_1:def 4;

                then

                 A39: (x `1 ) in (AA1 . (j,k)) by MCART_1: 10;

                then (x `1 ) in ( MSS_morph (j9,k9)) by A24;

                then

                consider g1,g2 be Function such that

                 A40: (x `1 ) = [g1, g2] and (g1,g2) form_morphism_between (j9,k9) by MSALIMIT:def 10;

                x in ( {|AA2, AA2|} . (i,j,k)) by A30, A37, MULTOP_1:def 1;

                then x in [:(AA2 . (j,k)), (AA2 . (i,j)):] by A32, ALTCAT_1:def 4;

                then

                 A41: (x `1 ) in (AA2 . (j,k)) & (x `2 ) in (AA2 . (i,j)) by MCART_1: 10;

                

                 A42: (x `2 ) in (AA1 . (i,j)) by A38, MCART_1: 10;

                then (x `2 ) in ( MSS_morph (i9,j9)) by A24;

                then

                consider f1,f2 be Function such that

                 A43: (x `2 ) = [f1, f2] and (f1,f2) form_morphism_between (i9,j9) by MSALIMIT:def 10;

                

                 A44: x = [ [g1, g2], [f1, f2]] by A38, A40, A43, MCART_1: 21;

                

                then (Ci . x) = ((the Comp of A1 . (I,J,K)) . ( [g1, g2], [f1, f2])) by MULTOP_1:def 1

                .= [(g1 * f1), (g2 * f2)] by A23, A25, A39, A42, A40, A43

                .= ((the Comp of A2 . (I9,J9,K9)) . ( [g1, g2], [f1, f2])) by A26, A28, A41, A40, A43

                .= (Cj . x) by A44, MULTOP_1:def 1;

                hence thesis;

              end;

              ( {|AA2|} . ijk) <> {} by A29, A35, ALTCAT_1: 7;

              then

               A45: ( dom Cj) = ( {|AA2, AA2|} . ijk) by FUNCT_2:def 1;

              ( dom Ci) = ( {|AA1, AA1|} . ijk) by A35, FUNCT_2:def 1;

              hence thesis by A30, A31, A34, A45, A36, FUNCT_1: 2;

            end;

              suppose ( {|AA1|} . ijk) = {} ;

              then Ci = {} & Cj = {} by A30;

              hence thesis by A31, MULTOP_1:def 1;

            end;

          end;

        end;

        hence thesis by A23, A26, A30, ALTCAT_1: 8;

      end;

    end

    registration

      let A;

      cluster ( MSSCat A) -> transitive associative with_units;

      coherence

      proof

        set M = ( MSSCat A);

        set G = ( MSSCat A);

        thus G is transitive

        proof

          let o1,o2,o3 be Object of G;

          reconsider o19 = o1, o29 = o2, o39 = o3 as Element of ( MSS_set A) by Def1;

          assume that

           A1: <^o1, o2^> <> {} and

           A2: <^o2, o3^> <> {} ;

          set s = the Element of ( MSS_morph (o29,o39));

          ( MSS_morph (o29,o39)) <> {} by A2, Def1;

          then

          consider u,w be Function such that s = [u, w] and

           A3: (u,w) form_morphism_between (o29,o39) by MSALIMIT:def 10;

          set t = the Element of ( MSS_morph (o19,o29));

          ( MSS_morph (o19,o29)) <> {} by A1, Def1;

          then

          consider f,g be Function such that t = [f, g] and

           A4: (f,g) form_morphism_between (o19,o29) by MSALIMIT:def 10;

          ((u * f),(w * g)) form_morphism_between (o19,o39) by A4, A3, PUA2MSS1: 29;

          then [(u * f), (w * g)] in ( MSS_morph (o19,o39)) by MSALIMIT:def 10;

          hence thesis by Def1;

        end;

        set G = the Arrows of M, C = the Comp of M;

        thus C is associative

        proof

          let i,j,k,l be Element of M;

          reconsider I = i, J = j, K = k, L = l as Object of M;

          let f,g,h be set;

          reconsider i9 = i, j9 = j, k9 = k, l9 = l as Element of ( MSS_set A) by Def1;

          assume that

           A5: f in (G . (i,j)) and

           A6: g in (G . (j,k)) and

           A7: h in (G . (k,l));

          g in ( MSS_morph (j9,k9)) by A6, Def1;

          then

          consider g1,g2 be Function such that

           A8: g = [g1, g2] and

           A9: (g1,g2) form_morphism_between (j9,k9) by MSALIMIT:def 10;

          f in ( MSS_morph (i9,j9)) by A5, Def1;

          then

          consider f1,f2 be Function such that

           A10: f = [f1, f2] and

           A11: (f1,f2) form_morphism_between (i9,j9) by MSALIMIT:def 10;

          

           A12: ((C . (i,j,k)) . (g,f)) = [(g1 * f1), (g2 * f2)] by A5, A6, A10, A11, A8, A9, Def1;

          h in ( MSS_morph (k9,l9)) by A7, Def1;

          then

          consider h1,h2 be Function such that

           A13: h = [h1, h2] and

           A14: (h1,h2) form_morphism_between (k9,l9) by MSALIMIT:def 10;

          

           A15: ((C . (j,k,l)) . (h,g)) = [(h1 * g1), (h2 * g2)] by A6, A7, A8, A9, A13, A14, Def1;

          ((h1 * g1),(h2 * g2)) form_morphism_between (j9,l9) by A9, A14, PUA2MSS1: 29;

          then [(h1 * g1), (h2 * g2)] in ( MSS_morph (j9,l9)) by MSALIMIT:def 10;

          then

           A16: [(h1 * g1), (h2 * g2)] in (G . (j,l)) by Def1;

          

           A17: ((h1 * g1) * f1) = (h1 * (g1 * f1)) & ((h2 * g2) * f2) = (h2 * (g2 * f2)) by RELAT_1: 36;

          J in the carrier of M;

          then

           A18: J in ( MSS_set A) by Def1;

          L in the carrier of M;

          then

           A19: L in ( MSS_set A) by Def1;

          ((g1 * f1),(g2 * f2)) form_morphism_between (i9,k9) by A11, A9, PUA2MSS1: 29;

          then [(g1 * f1), (g2 * f2)] in ( MSS_morph (i9,k9)) by MSALIMIT:def 10;

          then

           A20: [(g1 * f1), (g2 * f2)] in (G . (i,k)) by Def1;

          I in the carrier of M;

          then

           A21: I in ( MSS_set A) by Def1;

          K in the carrier of M;

          then K in ( MSS_set A) by Def1;

          then ((C . (i,k,l)) . (h, [(g1 * f1), (g2 * f2)])) = [(h1 * (g1 * f1)), (h2 * (g2 * f2))] by A21, A19, A7, A13, A20, Def1;

          hence thesis by A21, A18, A19, A5, A10, A12, A15, A16, A17, Def1;

        end;

        thus C is with_left_units

        proof

          let j be Element of M;

          reconsider j9 = j as Element of ( MSS_set A) by Def1;

          set e1 = ( id the carrier of j9), e2 = ( id the carrier' of j9);

          reconsider e = [e1, e2] as set;

          take e;

          (e1,e2) form_morphism_between (j9,j9) & (G . (j,j)) = ( MSS_morph (j9,j9)) by Def1, PUA2MSS1: 28;

          hence

           A22: e in (G . (j,j)) by MSALIMIT:def 10;

          let i be Element of M;

          reconsider i9 = i as Element of ( MSS_set A) by Def1;

          let f be set;

          reconsider I = i, J = j as Object of M;

          assume

           A23: f in (G . (i,j));

          then f in ( MSS_morph (i9,j9)) by Def1;

          then

          consider f1,f2 be Function such that

           A24: f = [f1, f2] and

           A25: (f1,f2) form_morphism_between (i9,j9) by MSALIMIT:def 10;

          

           A26: ( rng f2) c= the carrier' of j9 by A25, PUA2MSS1:def 12;

          ( rng f1) c= the carrier of j9 by A25, PUA2MSS1:def 12;

          then

           A27: (e1 * f1) = f1 by RELAT_1: 53;

          ((C . (I,J,J)) . ( [e1, e2], [f1, f2])) = [(e1 * f1), (e2 * f2)] by A22, A23, A24, A25, Def1;

          hence thesis by A24, A26, A27, RELAT_1: 53;

        end;

        thus C is with_right_units

        proof

          let i be Element of M;

          reconsider i9 = i as Element of ( MSS_set A) by Def1;

          set e1 = ( id the carrier of i9), e2 = ( id the carrier' of i9);

          reconsider e = [e1, e2] as set;

          take e;

          (e1,e2) form_morphism_between (i9,i9) & (G . (i,i)) = ( MSS_morph (i9,i9)) by Def1, PUA2MSS1: 28;

          hence

           A28: e in (G . (i,i)) by MSALIMIT:def 10;

          let j be Element of M;

          reconsider j9 = j as Element of ( MSS_set A) by Def1;

          let f be set;

          reconsider I = i, J = j as Object of M;

          assume

           A29: f in (G . (i,j));

          then f in ( MSS_morph (i9,j9)) by Def1;

          then

          consider f1,f2 be Function such that

           A30: f = [f1, f2] and

           A31: (f1,f2) form_morphism_between (i9,j9) by MSALIMIT:def 10;

          

           A32: ( dom f2) = the carrier' of i9 by A31, PUA2MSS1:def 12;

          ( dom f1) = the carrier of i9 by A31, PUA2MSS1:def 12;

          then

           A33: (f1 * e1) = f1 by RELAT_1: 52;

          ((C . (I,I,J)) . ( [f1, f2], [e1, e2])) = [(f1 * e1), (f2 * e2)] by A28, A29, A30, A31, Def1;

          hence thesis by A30, A32, A33, RELAT_1: 52;

        end;

      end;

    end

    theorem :: MSINST_1:1

    for C be category st C = ( MSSCat A) holds for o be Object of C holds o is non empty non void ManySortedSign

    proof

      let C be category;

      assume

       A1: C = ( MSSCat A);

      let o be Object of C;

      reconsider o as Element of ( MSS_set A) by A1, Def1;

      o is non empty non void ManySortedSign;

      hence thesis;

    end;

    registration

      let S;

      cluster strict feasible for MSAlgebra over S;

      existence

      proof

        set M = the feasible MSAlgebra over S;

        take E = the MSAlgebra of M;

        thus E is strict;

        now

          let o be OperSymbol of S;

          

           A1: ( Args (o,M)) = (((the Sorts of E # ) * the Arity of S) . o) by MSUALG_1:def 4

          .= ( Args (o,E)) by MSUALG_1:def 4;

          ( Result (o,M)) = ((the Sorts of E * the ResultSort of S) . o) by MSUALG_1:def 5

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

          hence ( Args (o,E)) <> {} implies ( Result (o,E)) <> {} by A1, MSUALG_6:def 1;

        end;

        hence thesis by MSUALG_6:def 1;

      end;

    end

    definition

      let S, A;

      :: MSINST_1:def2

      func MSAlg_set (S,A) -> set means

      : Def2: for x be object holds x in it iff ex M be strict feasible MSAlgebra over S st x = M & for C be Component of the Sorts of M holds C c= A;

      existence

      proof

        defpred P[ object, object] means ex M be strict feasible MSAlgebra over S st M = $2 & $1 = [the Sorts of M, the Charact of M];

        

         A1: for x,y,z be object st P[x, y] & P[x, z] holds y = z

        proof

          let x,y,z be object;

          given M be strict feasible MSAlgebra over S such that

           A2: M = y and

           A3: x = [the Sorts of M, the Charact of M];

          given N be strict feasible MSAlgebra over S such that

           A4: N = z and

           A5: x = [the Sorts of N, the Charact of N];

          the Sorts of M = the Sorts of N by A3, A5, XTUPLE_0: 1;

          hence thesis by A2, A3, A4, A5, XTUPLE_0: 1;

        end;

        consider X be set such that

         A6: for x be object holds x in X iff ex y be object st y in [:( Funcs (the carrier of S,( bool A))), ( Funcs (the carrier' of S,( PFuncs (( PFuncs ( NAT ,A)),A)))):] & P[y, x] from TARSKI:sch 1( A1);

        take X;

        thus for x be object holds x in X iff ex M be strict feasible MSAlgebra over S st x = M & for C be Component of the Sorts of M holds C c= A

        proof

          let x be object;

          hereby

            assume x in X;

            then

            consider y be object such that

             A7: y in [:( Funcs (the carrier of S,( bool A))), ( Funcs (the carrier' of S,( PFuncs (( PFuncs ( NAT ,A)),A)))):] and

             A8: P[y, x] by A6;

            consider M be strict feasible MSAlgebra over S such that

             A9: M = x and y = [the Sorts of M, the Charact of M] by A8;

            take M;

            thus x = M by A9;

            thus for C be Component of the Sorts of M holds C c= A

            proof

              let C be Component of the Sorts of M;

              consider y1 be object such that y1 in ( dom the Sorts of M) and

               A10: C = (the Sorts of M . y1) by FUNCT_1:def 3;

              the Sorts of M in ( Funcs (the carrier of S,( bool A))) by A7, A8, A9, ZFMISC_1: 87;

              then

              consider f be Function such that

               A11: the Sorts of M = f and ( dom f) = the carrier of S and

               A12: ( rng f) c= ( bool A) by FUNCT_2:def 2;

              (f . y1) in ( rng f) by A10, A11;

              hence thesis by A10, A11, A12;

            end;

          end;

          given M be strict feasible MSAlgebra over S such that

           A13: x = M and

           A14: for C be Component of the Sorts of M holds C c= A;

          

           A15: ( dom the Sorts of M) = the carrier of S by PARTFUN1:def 2;

          then

          reconsider SM = the Sorts of M as Function of the carrier of S, ( rng the Sorts of M) by FUNCT_2: 1;

          

           A16: ( rng the Sorts of M) c= ( bool A)

          proof

            let x be object;

            assume x in ( rng the Sorts of M);

            then

            reconsider x9 = x as Component of the Sorts of M;

            x9 c= A by A14;

            hence thesis;

          end;

          then

          reconsider SM9 = SM as Function of the carrier of S, ( bool A) by FUNCT_2: 6;

          consider y be set such that

           A17: y = [the Sorts of M, the Charact of M];

          

           A18: ( dom the Charact of M) = the carrier' of S by PARTFUN1:def 2;

          ( rng the Charact of M) c= ( PFuncs (( PFuncs ( NAT ,A)),A))

          proof

            reconsider SA = ((the Sorts of M # ) * the Arity of S), SR = (the Sorts of M * the ResultSort of S) as ManySortedSet of the carrier' of S;

            let x be object;

            reconsider CM = the Charact of M as ManySortedFunction of SA, SR;

            assume x in ( rng the Charact of M);

            then

            consider x1 be object such that

             A19: x1 in ( dom the Charact of M) and

             A20: x = (the Charact of M . x1) by FUNCT_1:def 3;

            reconsider Cm = (CM . x1) as Function of (SA . x1), (SR . x1) by A19, PBOOLE:def 15;

            

             A21: x1 in ( dom SA) by A18, A19, PARTFUN1:def 2;

            (SA . x1) c= ( PFuncs ( NAT ,A))

            proof

              reconsider AX = (the Arity of S . x1) as Element of (the carrier of S * ) by A19, FUNCT_2: 5;

              let a be object;

              assume a in (SA . x1);

              then

               A22: a in ((the Sorts of M # ) . (the Arity of S . x1)) by A21, FUNCT_1: 12;

              ((the Sorts of M # ) . AX) = ( product (the Sorts of M * AX)) by FINSEQ_2:def 5;

              then

               A23: ex g be Function st a = g & ( dom g) = ( dom (the Sorts of M * AX)) & for x2 be object st x2 in ( dom (the Sorts of M * AX)) holds (g . x2) in ((the Sorts of M * AX) . x2) by A22, CARD_3:def 5;

              then

              reconsider a9 = a as Function;

              ( rng AX) c= ( dom the Sorts of M) by A15;

              then

               A24: ( dom a9) = ( dom AX) by A23, RELAT_1: 27;

              ( rng a9) c= A

              proof

                ( rng the Sorts of M) c= ( bool A)

                proof

                  let w be object;

                  assume w in ( rng the Sorts of M);

                  then

                  reconsider w9 = w as Component of the Sorts of M;

                  w9 c= A by A14;

                  hence thesis;

                end;

                then

                 A25: ( union ( rng the Sorts of M)) c= ( union ( bool A)) by ZFMISC_1: 77;

                let r be object;

                assume r in ( rng a9);

                then

                consider r1 be object such that

                 A26: r1 in ( dom a9) and

                 A27: r = (a9 . r1) by FUNCT_1:def 3;

                (AX . r1) in ( rng AX) by A24, A26, FUNCT_1:def 3;

                then

                 A28: (the Sorts of M . (AX . r1)) in ( rng the Sorts of M) by A15, FUNCT_1:def 3;

                r in ((the Sorts of M * AX) . r1) by A23, A26, A27;

                then r in (the Sorts of M . (AX . r1)) by A24, A26, FUNCT_1: 13;

                then r in ( union ( rng the Sorts of M)) by A28, TARSKI:def 4;

                then r in ( union ( bool A)) by A25;

                hence thesis by ZFMISC_1: 81;

              end;

              hence thesis by A23, PARTFUN1:def 3;

            end;

            then

             A29: ( dom Cm) c= ( PFuncs ( NAT ,A));

            x1 in ( dom SR) by A18, A19, PARTFUN1:def 2;

            then

             A30: (SR . x1) = (the Sorts of M . (the ResultSort of S . x1)) by FUNCT_1: 12;

            (the ResultSort of S . x1) in the carrier of S by A19, FUNCT_2: 5;

            then (SR . x1) in ( rng the Sorts of M) by A15, A30, FUNCT_1:def 3;

            then ( rng Cm) c= A by A16, XBOOLE_1: 1;

            hence thesis by A20, A29, PARTFUN1:def 3;

          end;

          then SM9 in ( Funcs (the carrier of S,( bool A))) & the Charact of M in ( Funcs (the carrier' of S,( PFuncs (( PFuncs ( NAT ,A)),A)))) by A18, FUNCT_2: 8, FUNCT_2:def 2;

          then y in [:( Funcs (the carrier of S,( bool A))), ( Funcs (the carrier' of S,( PFuncs (( PFuncs ( NAT ,A)),A)))):] by A17, ZFMISC_1: 87;

          hence thesis by A6, A13, A17;

        end;

      end;

      uniqueness

      proof

        let A1,A2 be set;

        assume

         A31: for x be object holds x in A1 iff ex M be strict feasible MSAlgebra over S st x = M & for C be Component of the Sorts of M holds C c= A;

        assume

         A32: for x be object holds x in A2 iff ex N be strict feasible MSAlgebra over S st x = N & for C be Component of the Sorts of N holds C c= A;

        

         A33: A2 c= A1

        proof

          let a be object;

          assume a in A2;

          then ex M be strict feasible MSAlgebra over S st a = M & for C be Component of the Sorts of M holds C c= A by A32;

          hence thesis by A31;

        end;

        A1 c= A2

        proof

          let a be object;

          assume a in A1;

          then ex M be strict feasible MSAlgebra over S st a = M & for C be Component of the Sorts of M holds C c= A by A31;

          hence thesis by A32;

        end;

        hence A1 = A2 by A33, XBOOLE_0:def 10;

      end;

    end

    registration

      let S, A;

      cluster ( MSAlg_set (S,A)) -> non empty;

      coherence

      proof

        set a = the Element of A;

        reconsider f = (the carrier of S --> {a}) as ManySortedSet of the carrier of S;

        set Ch = the ManySortedFunction of ((f # ) * the Arity of S), (f * the ResultSort of S);

        set Ex = MSAlgebra (# f, Ch #);

        reconsider Ex as non-empty MSAlgebra over S by MSUALG_1:def 3;

        reconsider Ex as strict feasible MSAlgebra over S;

        for C be Component of the Sorts of Ex holds C c= A

        proof

          let C be Component of the Sorts of Ex;

          ex i be object st i in the carrier of S & C = (the Sorts of Ex . i) by PBOOLE: 138;

          then C = {a} by FUNCOP_1: 7;

          hence thesis by ZFMISC_1: 31;

        end;

        hence thesis by Def2;

      end;

    end

    begin

    reserve o for OperSymbol of S;

    theorem :: MSINST_1:2

    for x be MSAlgebra over S st x in ( MSAlg_set (S,A)) holds the Sorts of x in ( Funcs (the carrier of S,( bool A))) & the Charact of x in ( Funcs (the carrier' of S,( PFuncs (( PFuncs ( NAT ,A)),A))))

    proof

      let x be MSAlgebra over S;

      assume x in ( MSAlg_set (S,A));

      then

      consider M be strict feasible MSAlgebra over S such that

       A1: x = M and

       A2: for C be Component of the Sorts of M holds C c= A by Def2;

      

       A3: ( dom the Sorts of M) = the carrier of S by PARTFUN1:def 2;

      then

      reconsider SM = the Sorts of M as Function of the carrier of S, ( rng the Sorts of M) by FUNCT_2: 1;

      

       A4: ( rng the Sorts of M) c= ( bool A)

      proof

        let x be object;

        assume x in ( rng the Sorts of M);

        then

        reconsider x9 = x as Component of the Sorts of M;

        x9 c= A by A2;

        hence thesis;

      end;

      then

      reconsider SM9 = SM as Function of the carrier of S, ( bool A) by FUNCT_2: 6;

      

       A5: ( dom the Charact of M) = the carrier' of S by PARTFUN1:def 2;

      

       A6: ( rng the Charact of M) c= ( PFuncs (( PFuncs ( NAT ,A)),A))

      proof

        reconsider SA = ((the Sorts of M # ) * the Arity of S), SR = (the Sorts of M * the ResultSort of S) as ManySortedSet of the carrier' of S;

        let x be object;

        reconsider CM = the Charact of M as ManySortedFunction of SA, SR;

        assume x in ( rng the Charact of M);

        then

        consider x1 be object such that

         A7: x1 in ( dom the Charact of M) and

         A8: x = (the Charact of M . x1) by FUNCT_1:def 3;

        reconsider Cm = (CM . x1) as Function of (SA . x1), (SR . x1) by A7, PBOOLE:def 15;

        

         A9: x1 in ( dom SA) by A5, A7, PARTFUN1:def 2;

        (SA . x1) c= ( PFuncs ( NAT ,A))

        proof

          reconsider AX = (the Arity of S . x1) as Element of (the carrier of S * ) by A7, FUNCT_2: 5;

          let a be object;

          assume a in (SA . x1);

          then

           A10: a in ((the Sorts of M # ) . (the Arity of S . x1)) by A9, FUNCT_1: 12;

          ((the Sorts of M # ) . AX) = ( product (the Sorts of M * AX)) by FINSEQ_2:def 5;

          then

           A11: ex g be Function st a = g & ( dom g) = ( dom (the Sorts of M * AX)) & for x2 be object st x2 in ( dom (the Sorts of M * AX)) holds (g . x2) in ((the Sorts of M * AX) . x2) by A10, CARD_3:def 5;

          then

          reconsider a9 = a as Function;

          ( rng AX) c= ( dom the Sorts of M) by A3;

          then

           A12: ( dom a9) = ( dom AX) by A11, RELAT_1: 27;

          ( rng a9) c= A

          proof

            ( rng the Sorts of M) c= ( bool A)

            proof

              let w be object;

              assume w in ( rng the Sorts of M);

              then

              reconsider w9 = w as Component of the Sorts of M;

              w9 c= A by A2;

              hence thesis;

            end;

            then

             A13: ( union ( rng the Sorts of M)) c= ( union ( bool A)) by ZFMISC_1: 77;

            let r be object;

            assume r in ( rng a9);

            then

            consider r1 be object such that

             A14: r1 in ( dom a9) and

             A15: r = (a9 . r1) by FUNCT_1:def 3;

            (AX . r1) in ( rng AX) by A12, A14, FUNCT_1:def 3;

            then

             A16: (the Sorts of M . (AX . r1)) in ( rng the Sorts of M) by A3, FUNCT_1:def 3;

            r in ((the Sorts of M * AX) . r1) by A11, A14, A15;

            then r in (the Sorts of M . (AX . r1)) by A12, A14, FUNCT_1: 13;

            then r in ( union ( rng the Sorts of M)) by A16, TARSKI:def 4;

            then r in ( union ( bool A)) by A13;

            hence thesis by ZFMISC_1: 81;

          end;

          hence thesis by A11, PARTFUN1:def 3;

        end;

        then

         A17: ( dom Cm) c= ( PFuncs ( NAT ,A));

        x1 in ( dom SR) by A5, A7, PARTFUN1:def 2;

        then

         A18: (SR . x1) = (the Sorts of M . (the ResultSort of S . x1)) by FUNCT_1: 12;

        (the ResultSort of S . x1) in the carrier of S by A7, FUNCT_2: 5;

        then (SR . x1) in ( rng the Sorts of M) by A3, A18, FUNCT_1:def 3;

        then ( rng Cm) c= A by A4, XBOOLE_1: 1;

        hence thesis by A8, A17, PARTFUN1:def 3;

      end;

      SM9 in ( Funcs (the carrier of S,( bool A))) by FUNCT_2: 8;

      hence thesis by A1, A5, A6, FUNCT_2:def 2;

    end;

    theorem :: MSINST_1:3

    

     Th3: for U1,U2 be MSAlgebra over S st the Sorts of U1 is_transformable_to the Sorts of U2 & ( Args (o,U1)) <> {} holds ( Args (o,U2)) <> {}

    proof

      let U1,U2 be MSAlgebra over S;

      assume that

       A1: the Sorts of U1 is_transformable_to the Sorts of U2 and

       A2: ( Args (o,U1)) <> {} ;

      

       A3: (((the Sorts of U1 # ) * the Arity of S) . o) <> {} by A2, MSUALG_1:def 4;

      ( dom the Sorts of U1) = the carrier of S by PARTFUN1:def 2;

      then ( rng ( the_arity_of o)) c= ( dom the Sorts of U1);

      then

       A4: ( dom (the Sorts of U1 * ( the_arity_of o))) = ( dom ( the_arity_of o)) by RELAT_1: 27;

      

       A5: ( dom (the Sorts of U2 * ( the_arity_of o))) c= ( dom ( the_arity_of o)) by RELAT_1: 25;

      

       A6: ( dom the Arity of S) = the carrier' of S by FUNCT_2:def 1;

      

      then (((the Sorts of U1 # ) * the Arity of S) . o) = ((the Sorts of U1 # ) . (the Arity of S . o)) by FUNCT_1: 13

      .= ((the Sorts of U1 # ) . ( the_arity_of o)) by MSUALG_1:def 1;

      then ( product (the Sorts of U1 * ( the_arity_of o))) <> {} by A3, FINSEQ_2:def 5;

      then

       A7: not {} in ( rng (the Sorts of U1 * ( the_arity_of o))) by CARD_3: 26;

      now

        let x be object;

        assume

         A8: x in ( dom (the Sorts of U2 * ( the_arity_of o)));

        then (( the_arity_of o) . x) in ( rng ( the_arity_of o)) by A5, FUNCT_1:def 3;

        then

         A9: (the Sorts of U1 . (( the_arity_of o) . x)) <> {} implies (the Sorts of U2 . (( the_arity_of o) . x)) <> {} by A1, PZFMISC1:def 3;

        ((the Sorts of U1 * ( the_arity_of o)) . x) = (the Sorts of U1 . (( the_arity_of o) . x)) by A5, A8, FUNCT_1: 13;

        hence ((the Sorts of U2 * ( the_arity_of o)) . x) <> {} by A7, A4, A5, A8, A9, FUNCT_1: 13, FUNCT_1:def 3;

      end;

      then not {} in ( rng (the Sorts of U2 * ( the_arity_of o))) by FUNCT_1:def 3;

      then ( product (the Sorts of U2 * ( the_arity_of o))) <> {} by CARD_3: 26;

      then ((the Sorts of U2 # ) . ( the_arity_of o)) <> {} by FINSEQ_2:def 5;

      then ((the Sorts of U2 # ) . (the Arity of S . o)) <> {} by MSUALG_1:def 1;

      then (((the Sorts of U2 # ) * the Arity of S) . o) <> {} by A6, FUNCT_1: 13;

      hence thesis by MSUALG_1:def 4;

    end;

    theorem :: MSINST_1:4

    

     Th4: for U1,U2,U3 be feasible MSAlgebra over S, F be ManySortedFunction of U1, U2, G be ManySortedFunction of U2, U3, x be Element of ( Args (o,U1)) st ( Args (o,U1)) <> {} & the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 holds ex GF be ManySortedFunction of U1, U3 st GF = (G ** F) & (GF # x) = (G # (F # x))

    proof

      let U1,U2,U3 be feasible MSAlgebra over S, F be ManySortedFunction of U1, U2, G be ManySortedFunction of U2, U3, x be Element of ( Args (o,U1));

      assume that

       A1: ( Args (o,U1)) <> {} and

       A2: the Sorts of U1 is_transformable_to the Sorts of U2 and

       A3: the Sorts of U2 is_transformable_to the Sorts of U3;

      x in ( Args (o,U1)) by A1;

      then x in ( product (the Sorts of U1 * ( the_arity_of o))) by PRALG_2: 3;

      then

       A4: ex g be Function st x = g & ( dom g) = ( dom (the Sorts of U1 * ( the_arity_of o))) & for x be object st x in ( dom (the Sorts of U1 * ( the_arity_of o))) holds (g . x) in ((the Sorts of U1 * ( the_arity_of o)) . x) by CARD_3:def 5;

      then

      reconsider x9 = x as Function;

      reconsider Fr = (( Frege (F * ( the_arity_of o))) . x9) as Function;

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

      then

       A5: ( rng ( the_arity_of o)) c= ( dom F);

      then

       A6: ( dom (F * ( the_arity_of o))) = ( dom ( the_arity_of o)) by RELAT_1: 27;

      

       A7: ( dom ( doms (F * ( the_arity_of o)))) = ( dom (F * ( the_arity_of o))) by FUNCT_6: 59;

      then

       A8: ( dom x9) = ( dom ( doms (F * ( the_arity_of o)))) by A1, A6, MSUALG_3: 6;

      then

      reconsider x99 = x9 as ManySortedSet of ( dom ( the_arity_of o)) by A6, A7, PARTFUN1:def 2, RELAT_1:def 18;

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

      then ( rng ( the_arity_of o)) c= ( dom G);

      then

       A9: ( dom (G * ( the_arity_of o))) = ( dom ( the_arity_of o)) by RELAT_1: 27;

      then

      reconsider Ga = (G * ( the_arity_of o)), Fa = (F * ( the_arity_of o)) as ManySortedFunction of ( dom ( the_arity_of o)) by A6, PARTFUN1:def 2, RELAT_1:def 18;

      

       A10: ( Args (o,U2)) <> {} by A1, A2, Th3;

      ( dom the Sorts of U1) = the carrier of S by PARTFUN1:def 2;

      then

       A11: ( rng ( the_arity_of o)) c= ( dom the Sorts of U1);

      now

        let x be object;

        set ds = (( the_arity_of o) . x);

        assume x in ( dom ( doms (F * ( the_arity_of o))));

        then

         A12: x in ( dom (F * ( the_arity_of o))) by FUNCT_6: 59;

        then

         A13: (( doms (F * ( the_arity_of o))) . x) = ( dom ((F * ( the_arity_of o)) . x)) by FUNCT_6: 22;

        

         A14: x in ( dom ( the_arity_of o)) by A5, A12, RELAT_1: 27;

        then

         A15: ds in ( rng ( the_arity_of o)) by FUNCT_1:def 3;

        then

        reconsider Ff = (F . ds) as Function of (the Sorts of U1 . ds), (the Sorts of U2 . ds) by PBOOLE:def 15;

        x in ( dom (the Sorts of U1 * ( the_arity_of o))) by A11, A14, RELAT_1: 27;

        then

         A16: (x9 . x) in ((the Sorts of U1 * ( the_arity_of o)) . x) by A1, MSUALG_3: 6;

        

         A17: (the Sorts of U1 . ds) = ( dom Ff)

        proof

          per cases ;

            suppose (the Sorts of U2 . ds) <> {} ;

            hence thesis by FUNCT_2:def 1;

          end;

            suppose (the Sorts of U2 . ds) = {} ;

            then (the Sorts of U1 . ds) = {} by A2, A15, PZFMISC1:def 3;

            hence thesis;

          end;

        end;

        ((F * ( the_arity_of o)) . x) = (F . (( the_arity_of o) . x)) by A14, FUNCT_1: 13;

        hence (x9 . x) in (( doms (F * ( the_arity_of o))) . x) by A13, A14, A16, A17, FUNCT_1: 13;

      end;

      then

       A18: x9 in ( product ( doms (F * ( the_arity_of o)))) by A8, CARD_3: 9;

      then

       A19: Fr = ((F * ( the_arity_of o)) .. x9) by PRALG_2:def 2;

       A20:

      now

        let x be object;

        set ds = (( the_arity_of o) . x);

        assume

         A21: x in ( dom ( doms (G * ( the_arity_of o))));

        then

         A22: x in ( dom (G * ( the_arity_of o))) by FUNCT_6: 59;

        

         Z2: ( dom x9) = ( dom ( the_arity_of o)) by A1, MSUALG_3: 6;

        

         Z1: x in ( dom (F * ( the_arity_of o))) by A9, A6, A21, FUNCT_6: 59;

        

         Z3: ( dom (F * ( the_arity_of o))) = ( dom ( the_arity_of o)) by A6;

        then

         Z4: (( dom (F * ( the_arity_of o))) /\ ( dom x9)) = ( dom ( the_arity_of o)) by Z2;

        then x in (( dom (F * ( the_arity_of o))) /\ ( dom x9)) by Z1, Z3;

        then x in ( dom ((F * ( the_arity_of o)) .. x9)) by PRALG_1:def 19;

        then

         A23: (Fr . x) = (((F * ( the_arity_of o)) . x) . (x9 . x)) by A19, PRALG_1:def 19;

        

         A24: ( dom (the Sorts of U1 * ( the_arity_of o))) = ( dom ( the_arity_of o)) by A11, RELAT_1: 27;

        

         A25: x in ( dom ( the_arity_of o)) by A9, A21, FUNCT_6: 59;

        then

         A26: ds in ( rng ( the_arity_of o)) by FUNCT_1:def 3;

        then

        reconsider Ff = (F . ds) as Function of (the Sorts of U1 . ds), (the Sorts of U2 . ds) by PBOOLE:def 15;

        

         A27: ((F * ( the_arity_of o)) . x) = Ff by A6, A25, FUNCT_1: 12;

        reconsider Gds = (G . ds) as Function of (the Sorts of U2 . ds), (the Sorts of U3 . ds) by A26, PBOOLE:def 15;

        

         A28: ( dom Gds) = (the Sorts of U2 . ds)

        proof

          per cases ;

            suppose (the Sorts of U3 . ds) <> {} ;

            hence thesis by FUNCT_2:def 1;

          end;

            suppose (the Sorts of U3 . ds) = {} ;

            then (the Sorts of U2 . ds) = {} by A3, A26, PZFMISC1:def 3;

            hence thesis;

          end;

        end;

        

         A29: (the Sorts of U1 . ds) = ( dom Ff)

        proof

          per cases ;

            suppose (the Sorts of U2 . ds) <> {} ;

            hence thesis by FUNCT_2:def 1;

          end;

            suppose (the Sorts of U2 . ds) = {} ;

            then (the Sorts of U1 . ds) = {} by A2, A26, PZFMISC1:def 3;

            hence thesis;

          end;

        end;

        ((the Sorts of U1 * ( the_arity_of o)) . x) = (the Sorts of U1 . (( the_arity_of o) . x)) by A25, FUNCT_1: 13;

        then (x9 . x) in ( dom Ff) by A1, A25, A24, A29, MSUALG_3: 6;

        then

         A30: (((F * ( the_arity_of o)) . x) . (x9 . x)) in ( rng Ff) by A27, FUNCT_1:def 3;

        ((G * ( the_arity_of o)) . x) = (G . (( the_arity_of o) . x)) by A25, FUNCT_1: 13;

        then (Fr . x) in ( dom ((G * ( the_arity_of o)) . x)) by A28, A30, A23;

        hence (Fr . x) in (( doms (G * ( the_arity_of o))) . x) by A22, FUNCT_6: 22;

      end;

      reconsider GF = (G ** F) as ManySortedFunction of U1, U3 by A2, ALTCAT_2: 4;

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

      then ( rng ( the_arity_of o)) c= ( dom GF);

      then

       A31: ( dom (GF * ( the_arity_of o))) = ( dom ( the_arity_of o)) by RELAT_1: 27;

      

       A32: x99 in ( doms Fa)

      proof

        let i be object;

        set ai = (( the_arity_of o) . i);

        assume

         A33: i in ( dom ( the_arity_of o));

        then

         A34: ai in ( rng ( the_arity_of o)) by FUNCT_1:def 3;

        (Fa . i) = (F . (( the_arity_of o) . i)) by A33, FUNCT_1: 13;

        then

        reconsider Ew = (Fa . i) as Function of (the Sorts of U1 . ai), (the Sorts of U2 . ai) by A34, PBOOLE:def 15;

        

         A35: ( dom Ew) = (the Sorts of U1 . ai)

        proof

          per cases ;

            suppose (the Sorts of U2 . ai) = {} ;

            then (the Sorts of U1 . ai) = {} by A2, A34, PZFMISC1:def 3;

            hence thesis;

          end;

            suppose (the Sorts of U2 . ai) <> {} ;

            hence thesis by FUNCT_2:def 1;

          end;

        end;

        i in ( dom (the Sorts of U1 * ( the_arity_of o))) by A33, PRALG_2: 3;

        then (x99 . i) in ((the Sorts of U1 * ( the_arity_of o)) . i) by A4;

        then (x99 . i) in ( dom (Fa . i)) by A33, A35, FUNCT_1: 13;

        hence thesis by A33, MSSUBFAM: 14;

      end;

      take GF;

      thus GF = (G ** F);

      

       A36: ((G * ( the_arity_of o)) ** (F * ( the_arity_of o))) = (GF * ( the_arity_of o)) by FUNCTOR0: 12;

      

       A37: the Sorts of U1 is_transformable_to the Sorts of U3 by A2, A3, AUTALG_1: 10;

      set tao = ( the_arity_of o);

       A38:

      now

        let x be object;

        set ds = (tao . x);

        assume

         A39: x in ( dom ( doms (GF * tao)));

        then

         A40: x in ( dom tao) by A31, FUNCT_6: 59;

        then

         A41: ds in ( rng tao) by FUNCT_1:def 3;

        then

        reconsider Gf = (GF . ds) as Function of (the Sorts of U1 . ds), (the Sorts of U3 . ds) by PBOOLE:def 15;

        x in ( dom (GF * tao)) by A39, FUNCT_6: 59;

        then

         A42: (( doms (GF * tao)) . x) = ( dom ((GF * tao) . x)) by FUNCT_6: 22;

        

         A43: (the Sorts of U1 . ds) = ( dom Gf)

        proof

          per cases ;

            suppose (the Sorts of U3 . ds) <> {} ;

            hence thesis by FUNCT_2:def 1;

          end;

            suppose (the Sorts of U3 . ds) = {} ;

            then (the Sorts of U1 . ds) = {} by A37, A41, PZFMISC1:def 3;

            hence thesis;

          end;

        end;

        x in ( dom (the Sorts of U1 * tao)) by A11, A40, RELAT_1: 27;

        then (x9 . x) in ((the Sorts of U1 * tao) . x) by A1, MSUALG_3: 6;

        then (x9 . x) in ( dom (GF . ds)) by A40, A43, FUNCT_1: 13;

        hence (x9 . x) in (( doms (GF * tao)) . x) by A42, A40, FUNCT_1: 13;

      end;

      ( dom ( doms (GF * tao))) = ( dom (GF * tao)) by FUNCT_6: 59;

      then ( dom x9) = ( dom ( doms (GF * tao))) by A1, A31, MSUALG_3: 6;

      then

       A44: x9 in ( product ( doms (GF * tao))) by A38, CARD_3: 9;

      ( rng tao) c= ( dom F) by A5;

      then

       S2: ( dom (F * tao)) = ( dom tao) by RELAT_1: 27;

      

       S0: ( dom tao) = ( dom x99) by A1, MSUALG_3: 6;

      ( dom Fr) = (( dom (F * tao)) /\ ( dom x99)) by A19, PRALG_1:def 19

      .= ( dom (G * tao)) by A9, S0, S2;

      then ( dom Fr) = ( dom ( doms (G * tao))) by FUNCT_6: 59;

      then Fr in ( product ( doms (G * tao))) by A20, CARD_3: 9;

      

      then

       A45: (( Frege (G * tao)) . (( Frege (F * tao)) . x)) = ((G * tao) .. (( Frege (F * tao)) . x)) by PRALG_2:def 2

      .= (Ga .. (Fa .. x99)) by A18, PRALG_2:def 2

      .= ((Ga ** Fa) .. x99) by A32, CLOSURE1: 4;

      

       A46: ( Args (o,U3)) <> {} by A1, A2, A3, Th3, AUTALG_1: 10;

      

      then (GF # x) = (( Frege (GF * tao)) . x) by A1, MSUALG_3:def 5

      .= (( Frege (G * tao)) . (( Frege (F * tao)) . x)) by A44, A45, A36, PRALG_2:def 2

      .= (( Frege (G * tao)) . (F # x)) by A1, A10, MSUALG_3:def 5;

      hence thesis by A10, A46, MSUALG_3:def 5;

    end;

    theorem :: MSINST_1:5

    

     Th5: for U1,U2,U3 be feasible MSAlgebra over S, F be ManySortedFunction of U1, U2, G be ManySortedFunction of U2, U3 st the Sorts of U1 is_transformable_to the Sorts of U2 & the Sorts of U2 is_transformable_to the Sorts of U3 & F is_homomorphism (U1,U2) & G is_homomorphism (U2,U3) holds ex GF be ManySortedFunction of U1, U3 st GF = (G ** F) & GF is_homomorphism (U1,U3)

    proof

      let U1,U2,U3 be feasible MSAlgebra over S, F be ManySortedFunction of U1, U2, G be ManySortedFunction of U2, U3;

      assume that

       A1: the Sorts of U1 is_transformable_to the Sorts of U2 and

       A2: the Sorts of U2 is_transformable_to the Sorts of U3 and

       A3: F is_homomorphism (U1,U2) and

       A4: G is_homomorphism (U2,U3);

      reconsider GF = (G ** F) as ManySortedFunction of U1, U3 by A1, ALTCAT_2: 4;

      take GF;

      thus GF = (G ** F);

      thus GF is_homomorphism (U1,U3)

      proof

        let o be OperSymbol of S such that

         A5: ( Args (o,U1)) <> {} ;

        let x be Element of ( Args (o,U1));

        

         A6: ex gf be ManySortedFunction of U1, U3 st gf = (G ** F) & (gf # x) = (G # (F # x)) by A1, A2, A5, Th4;

        set r = ( the_result_sort_of o);

        ((F . r) . (( Den (o,U1)) . x)) = (( Den (o,U2)) . (F # x)) & ( Args (o,U2)) <> {} by A1, A3, A5, Th3;

        then

         A7: ((G . r) . ((F . r) . (( Den (o,U1)) . x))) = (( Den (o,U3)) . (G # (F # x))) by A4;

        

         A8: the Sorts of U1 is_transformable_to the Sorts of U3 by A1, A2, AUTALG_1: 10;

        

         A9: ( dom (GF . r)) = (the Sorts of U1 . r)

        proof

          per cases ;

            suppose (the Sorts of U1 . r) <> {} ;

            then (the Sorts of U3 . r) <> {} by A8, PZFMISC1:def 3;

            hence thesis by FUNCT_2:def 1;

          end;

            suppose (the Sorts of U1 . r) = {} ;

            hence thesis;

          end;

        end;

        o in the carrier' of S;

        then

         A10: o in ( dom the ResultSort of S) by FUNCT_2:def 1;

        ( rng the ResultSort of S) c= the carrier of S;

        then ( rng the ResultSort of S) c= ( dom the Sorts of U1) by PARTFUN1:def 2;

        then ( Result (o,U1)) = ((the Sorts of U1 * the ResultSort of S) . o) & ( dom (the Sorts of U1 * the ResultSort of S)) = ( dom the ResultSort of S) by MSUALG_1:def 5, RELAT_1: 27;

        

        then

         A11: ( Result (o,U1)) = (the Sorts of U1 . (the ResultSort of S . o)) by A10, FUNCT_1: 12

        .= (the Sorts of U1 . r) by MSUALG_1:def 2;

        then (GF . r) = ((G . r) * (F . r)) & (the Sorts of U1 . r) <> {} by A5, MSUALG_3: 2, MSUALG_6:def 1;

        hence thesis by A5, A7, A9, A11, A6, FUNCT_1: 12, FUNCT_2: 5;

      end;

    end;

    definition

      let S, A;

      let i,j be set;

      assume that

       A1: i in ( MSAlg_set (S,A)) and

       A2: j in ( MSAlg_set (S,A));

      :: MSINST_1:def3

      func MSAlg_morph (S,A,i,j) -> set means

      : Def3: x in it iff ex M,N be strict feasible MSAlgebra over S, f be ManySortedFunction of M, N st M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism (M,N);

      existence

      proof

        consider M be strict feasible MSAlgebra over S such that

         A3: i = M and

         A4: for C be Component of the Sorts of M holds C c= A by A1, Def2;

        consider N be strict feasible MSAlgebra over S such that

         A5: j = N and

         A6: for C be Component of the Sorts of N holds C c= A by A2, Def2;

        defpred P[ object] means the Sorts of M is_transformable_to the Sorts of N & ex f be ManySortedFunction of M, N st $1 = f & f is_homomorphism (M,N);

        consider X be set such that

         A7: for x be object holds x in X iff x in ( Funcs (the carrier of S,( PFuncs (( union ( bool A)),( union ( bool A)))))) & P[x] from XBOOLE_0:sch 1;

        take X;

        let x;

        hereby

          assume

           A8: x in X;

          then

          consider f be ManySortedFunction of M, N such that

           A9: x = f and

           A10: f is_homomorphism (M,N) by A7;

          take M, N;

          reconsider f as ManySortedFunction of M, N;

          take f;

          thus M = i & N = j & f = x by A3, A5, A9;

          thus the Sorts of M is_transformable_to the Sorts of N by A8, A7;

          thus f is_homomorphism (M,N) by A10;

        end;

        given M1,N1 be strict feasible MSAlgebra over S, f be ManySortedFunction of M1, N1 such that

         A11: M1 = i & N1 = j & f = x & the Sorts of M1 is_transformable_to the Sorts of N1 & f is_homomorphism (M1,N1);

        reconsider F = f as ManySortedFunction of M, N by A11, A3, A5;

        

         A12: ( dom F) = the carrier of S by PARTFUN1:def 2;

        ( rng F) c= ( PFuncs (( union ( bool A)),( union ( bool A))))

        proof

          

           A13: ( rng the Sorts of M) c= ( bool A)

          proof

            let x be object;

            assume x in ( rng the Sorts of M);

            then

            reconsider x9 = x as Component of the Sorts of M;

            x9 c= A by A4;

            hence thesis;

          end;

          let w be object;

          assume w in ( rng F);

          then

          consider w1 be object such that

           A14: w1 in ( dom F) and

           A15: w = (F . w1) by FUNCT_1:def 3;

          reconsider w9 = w as Function of (the Sorts of M . w1), (the Sorts of N . w1) by A14, A15, PBOOLE:def 15;

          

           A16: ( dom the Sorts of M) = the carrier of S by PARTFUN1:def 2;

          

           A17: ( dom w9) c= ( union ( bool A))

          proof

            let s be object;

            assume

             A18: s in ( dom w9);

            (the Sorts of M . w1) in ( rng the Sorts of M) by A14, A16, FUNCT_1:def 3;

            hence thesis by A13, A18, TARSKI:def 4;

          end;

          

           A19: ( rng the Sorts of N) c= ( bool A)

          proof

            let x be object;

            assume x in ( rng the Sorts of N);

            then

            reconsider x9 = x as Component of the Sorts of N;

            x9 c= A by A6;

            hence thesis;

          end;

          

           A20: ( dom the Sorts of N) = the carrier of S by PARTFUN1:def 2;

          ( rng w9) c= ( union ( bool A))

          proof

            let r be object;

            assume

             A21: r in ( rng w9);

            (the Sorts of N . w1) in ( rng the Sorts of N) by A14, A20, FUNCT_1:def 3;

            hence thesis by A19, A21, TARSKI:def 4;

          end;

          hence thesis by A17, PARTFUN1:def 3;

        end;

        then F in ( Funcs (the carrier of S,( PFuncs (( union ( bool A)),( union ( bool A)))))) by A12, FUNCT_2:def 2;

        hence x in X by A7, A11, A3, A5;

      end;

      uniqueness

      proof

        let A1,A2 be set;

        assume

         A22: x in A1 iff ex M,N be strict feasible MSAlgebra over S, f be ManySortedFunction of M, N st M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism (M,N);

        assume

         A23: x in A2 iff ex M,N be strict feasible MSAlgebra over S, f be ManySortedFunction of M, N st M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism (M,N);

        

         A24: A2 c= A1

        proof

          let a be object;

          assume a in A2;

          then ex M,N be strict feasible MSAlgebra over S, f be ManySortedFunction of M, N st M = i & N = j & f = a & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism (M,N) by A23;

          hence thesis by A22;

        end;

        A1 c= A2

        proof

          let a be object;

          assume a in A1;

          then ex M,N be strict feasible MSAlgebra over S, f be ManySortedFunction of M, N st M = i & N = j & f = a & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism (M,N) by A22;

          hence thesis by A23;

        end;

        hence A1 = A2 by A24, XBOOLE_0:def 10;

      end;

    end

    definition

      let S, A;

      :: MSINST_1:def4

      func MSAlgCat (S,A) -> strict non empty AltCatStr means

      : Def4: the carrier of it = ( MSAlg_set (S,A)) & (for i,j be Element of ( MSAlg_set (S,A)) holds (the Arrows of it . (i,j)) = ( MSAlg_morph (S,A,i,j))) & for i,j,k be Object of it , f,g be Function-yielding Function st f in (the Arrows of it . (i,j)) & g in (the Arrows of it . (j,k)) holds ((the Comp of it . (i,j,k)) . (g,f)) = (g ** f);

      existence

      proof

        set c = ( MSAlg_set (S,A));

        deffunc F( Element of c, Element of c) = ( MSAlg_morph (S,A,$1,$2));

        consider M be ManySortedSet of [:c, c:] such that

         A1: for i,j be Element of c holds (M . (i,j)) = F(i,j) from ALTCAT_1:sch 2;

        defpred P[ object, object, object] means ex i,j,k be Element of c st $3 = [i, j, k] & for f,g be Function-yielding Function st f in (M . (i,j)) & g in (M . (j,k)) & $2 = [g, f] holds $1 = (g ** f);

        

         A2: for ijk be object st ijk in [:c, c, c:] holds for x be object st x in ( {|M, M|} . ijk) holds ex y be object st y in ( {|M|} . ijk) & P[y, x, ijk]

        proof

          let ijk be object;

          assume ijk in [:c, c, c:];

          then

          consider x1,x2,x3 be object such that

           A3: x1 in c & x2 in c & x3 in c and

           A4: ijk = [x1, x2, x3] by MCART_1: 68;

          reconsider x1, x2, x3 as Element of c by A3;

          let x be object;

          

           A5: ( {|M, M|} . (x1,x2,x3)) = ( {|M, M|} . [x1, x2, x3]) & ( {|M, M|} . (x1,x2,x3)) = [:(M . (x2,x3)), (M . (x1,x2)):] by ALTCAT_1:def 4, MULTOP_1:def 1;

          

           A6: ( {|M|} . ijk) = ( {|M|} . (x1,x2,x3)) by A4, MULTOP_1:def 1;

          assume

           A7: x in ( {|M, M|} . ijk);

          then (x `1 ) in (M . (x2,x3)) by A4, A5, MCART_1: 10;

          then (x `1 ) in ( MSAlg_morph (S,A,x2,x3)) by A1;

          then

          consider M2,N2 be strict feasible MSAlgebra over S, g be ManySortedFunction of M2, N2 such that

           A8: M2 = x2 and

           A9: N2 = x3 and

           A10: g = (x `1 ) and

           A11: the Sorts of M2 is_transformable_to the Sorts of N2 & g is_homomorphism (M2,N2) by Def3;

          (x `2 ) in (M . (x1,x2)) by A4, A7, A5, MCART_1: 10;

          then (x `2 ) in ( MSAlg_morph (S,A,x1,x2)) by A1;

          then

          consider M1,N1 be strict feasible MSAlgebra over S, f be ManySortedFunction of M1, N1 such that

           A12: M1 = x1 and

           A13: N1 = x2 and

           A14: f = (x `2 ) and

           A15: the Sorts of M1 is_transformable_to the Sorts of N1 & f is_homomorphism (M1,N1) by Def3;

          take y = (g ** f);

          reconsider f as ManySortedFunction of M1, M2 by A8, A13;

          the Sorts of M1 is_transformable_to the Sorts of N2 & ex fg be ManySortedFunction of M1, N2 st fg = (g ** f) & fg is_homomorphism (M1,N2) by A8, A11, A13, A15, Th5, AUTALG_1: 10;

          then ( {|M|} . (x1,x2,x3)) = (M . (x1,x3)) & y in ( MSAlg_morph (S,A,x1,x3)) by A9, A12, Def3, ALTCAT_1:def 3;

          hence y in ( {|M|} . ijk) by A1, A6;

          take x1, x2, x3;

          thus ijk = [x1, x2, x3] by A4;

          let F,G be Function-yielding Function;

          assume that F in (M . (x1,x2)) and G in (M . (x2,x3)) and

           A16: x = [G, F];

          thus thesis by A10, A14, A16;

        end;

        consider F be ManySortedFunction of {|M, M|}, {|M|} such that

         A17: for ijk be object st ijk in [:c, c, c:] holds ex f be Function of ( {|M, M|} . ijk), ( {|M|} . ijk) st f = (F . ijk) & for x be object st x in ( {|M, M|} . ijk) holds P[(f . x), x, ijk] from MSSUBFAM:sch 1( A2);

        take EX = AltCatStr (# c, M, F #);

        reconsider EX as non empty AltCatStr;

        for i,j,k be Object of EX, f,g be Function-yielding Function st f in (the Arrows of EX . (i,j)) & g in (the Arrows of EX . (j,k)) holds ((the Comp of EX . (i,j,k)) . (g,f)) = (g ** f)

        proof

          let i,j,k be Object of EX, f,g be Function-yielding Function;

          assume

           A18: f in (the Arrows of EX . (i,j)) & g in (the Arrows of EX . (j,k));

          set x = [g, f];

          set ijk = [i, j, k];

          ijk in [:c, c, c:] by MCART_1: 69;

          then

          consider ff be Function of ( {|M, M|} . ijk), ( {|M|} . ijk) such that

           A19: ff = (F . ijk) and

           A20: for x be object st x in ( {|M, M|} . ijk) holds P[(ff . x), x, ijk] by A17;

          

           A21: ff = (the Comp of EX . (i,j,k)) by A19, MULTOP_1:def 1;

          ( {|M, M|} . (i,j,k)) = ( {|M, M|} . [i, j, k]) & ( {|M, M|} . (i,j,k)) = [:(M . (j,k)), (M . (i,j)):] by ALTCAT_1:def 4, MULTOP_1:def 1;

          then x in ( {|M, M|} . ijk) by A18, ZFMISC_1: 87;

          then

          consider I,J,K be Element of c such that

           A22: ijk = [I, J, K] and

           A23: for f,g be Function-yielding Function st f in (M . (I,J)) & g in (M . (J,K)) & x = [g, f] holds (ff . x) = (g ** f) by A20;

          

           A24: K = k by A22, XTUPLE_0: 3;

          I = i & J = j by A22, XTUPLE_0: 3;

          hence thesis by A18, A23, A24, A21;

        end;

        hence thesis by A1;

      end;

      uniqueness

      proof

        reconsider c = ( MSAlg_set (S,A)) as non empty set;

        let A1,A2 be non empty strict AltCatStr such that

         A25: the carrier of A1 = ( MSAlg_set (S,A)) and

         A26: for i,j be Element of ( MSAlg_set (S,A)) holds (the Arrows of A1 . (i,j)) = ( MSAlg_morph (S,A,i,j)) and

         A27: for i,j,k be Object of A1, f,g be Function-yielding Function st f in (the Arrows of A1 . (i,j)) & g in (the Arrows of A1 . (j,k)) holds ((the Comp of A1 . (i,j,k)) . (g,f)) = (g ** f) and

         A28: the carrier of A2 = ( MSAlg_set (S,A)) and

         A29: for i,j be Element of ( MSAlg_set (S,A)) holds (the Arrows of A2 . (i,j)) = ( MSAlg_morph (S,A,i,j)) and

         A30: for i,j,k be Object of A2, f,g be Function-yielding Function st f in (the Arrows of A2 . (i,j)) & g in (the Arrows of A2 . (j,k)) holds ((the Comp of A2 . (i,j,k)) . (g,f)) = (g ** f);

        reconsider CC1 = the Comp of A1, CC2 = the Comp of A2 as ManySortedSet of [:c, c, c:] by A25, A28;

        reconsider AA1 = the Arrows of A1, AA2 = the Arrows of A2 as ManySortedSet of [:c, c:] by A25, A28;

         A31:

        now

          let i,j be Element of c;

          

          thus (AA1 . (i,j)) = ( MSAlg_morph (S,A,i,j)) by A26

          .= (AA2 . (i,j)) by A29;

        end;

        then

         A32: AA1 = AA2 by ALTCAT_1: 7;

        now

          let i,j,k be object;

          set ijk = [i, j, k];

          

           A33: (CC1 . (i,j,k)) = (CC1 . [i, j, k]) by MULTOP_1:def 1;

          assume

           A34: i in c & j in c & k in c;

          then

          reconsider i9 = i, j9 = j, k9 = k as Element of c;

          reconsider I9 = i, J9 = j, K9 = k as Object of A2 by A28, A34;

          reconsider I = i, J = j, K = k as Object of A1 by A25, A34;

          

           A35: ijk in [:c, c, c:] by A34, MCART_1: 69;

          

           A36: (CC2 . (i,j,k)) = (CC2 . [i, j, k]) by MULTOP_1:def 1;

          thus (CC1 . (i,j,k)) = (CC2 . (i,j,k))

          proof

            reconsider Cj = (CC2 . ijk) as Function of ( {|AA2, AA2|} . ijk), ( {|AA2|} . ijk) by A28, A35, PBOOLE:def 15;

            reconsider Ci = (CC1 . ijk) as Function of ( {|AA1, AA1|} . ijk), ( {|AA1|} . ijk) by A25, A35, PBOOLE:def 15;

            per cases ;

              suppose

               A37: ( {|AA1|} . ijk) <> {} ;

              

               A38: for x be object st x in ( {|AA1, AA1|} . ijk) holds (Ci . x) = (Cj . x)

              proof

                let x be object;

                assume

                 A39: x in ( {|AA1, AA1|} . ijk);

                then x in ( {|AA1, AA1|} . (i,j,k)) by MULTOP_1:def 1;

                then

                 A40: x in [:(AA1 . (j,k)), (AA1 . (i,j)):] by A34, ALTCAT_1:def 4;

                then

                 A41: (x `1 ) in (AA1 . (j,k)) by MCART_1: 10;

                then (x `1 ) in ( MSAlg_morph (S,A,j9,k9)) by A26;

                then

                consider M2,N2 be strict feasible MSAlgebra over S, g be ManySortedFunction of M2, N2 such that M2 = j9 and N2 = k9 and

                 A42: g = (x `1 ) and the Sorts of M2 is_transformable_to the Sorts of N2 and g is_homomorphism (M2,N2) by Def3;

                x in ( {|AA2, AA2|} . (i,j,k)) by A32, A39, MULTOP_1:def 1;

                then x in [:(AA2 . (j,k)), (AA2 . (i,j)):] by A34, ALTCAT_1:def 4;

                then

                 A43: (x `1 ) in (AA2 . (j,k)) & (x `2 ) in (AA2 . (i,j)) by MCART_1: 10;

                

                 A44: (x `2 ) in (AA1 . (i,j)) by A40, MCART_1: 10;

                then (x `2 ) in ( MSAlg_morph (S,A,i9,j9)) by A26;

                then

                consider M1,N1 be strict feasible MSAlgebra over S, f be ManySortedFunction of M1, N1 such that M1 = i9 and N1 = j9 and

                 A45: f = (x `2 ) and the Sorts of M1 is_transformable_to the Sorts of N1 and f is_homomorphism (M1,N1) by Def3;

                

                 A46: x = [g, f] by A40, A45, A42, MCART_1: 21;

                

                then (Ci . x) = ((the Comp of A1 . (I,J,K)) . (g,f)) by MULTOP_1:def 1

                .= (g ** f) by A27, A41, A44, A45, A42

                .= ((the Comp of A2 . (I9,J9,K9)) . (g,f)) by A30, A43, A45, A42

                .= (Cj . x) by A46, MULTOP_1:def 1;

                hence thesis;

              end;

              ( {|AA2|} . ijk) <> {} by A31, A37, ALTCAT_1: 7;

              then

               A47: ( dom Cj) = ( {|AA2, AA2|} . ijk) by FUNCT_2:def 1;

              ( dom Ci) = ( {|AA1, AA1|} . ijk) by A37, FUNCT_2:def 1;

              hence thesis by A32, A33, A36, A47, A38, FUNCT_1: 2;

            end;

              suppose ( {|AA1|} . ijk) = {} ;

              then Ci = {} & Cj = {} by A32;

              hence thesis by A33, MULTOP_1:def 1;

            end;

          end;

        end;

        hence thesis by A25, A28, A32, ALTCAT_1: 8;

      end;

    end

    registration

      let S, A;

      cluster ( MSAlgCat (S,A)) -> transitive associative with_units;

      coherence

      proof

        set M = ( MSAlgCat (S,A));

        set G = ( MSAlgCat (S,A));

        set GM = the Arrows of M, C = the Comp of M;

        thus G is transitive

        proof

          let o1,o2,o3 be Object of G;

          reconsider o19 = o1, o29 = o2, o39 = o3 as Element of ( MSAlg_set (S,A)) by Def4;

          assume that

           A1: <^o1, o2^> <> {} and

           A2: <^o2, o3^> <> {} ;

          set t = the Element of ( MSAlg_morph (S,A,o19,o29));

          ( MSAlg_morph (S,A,o19,o29)) <> {} by A1, Def4;

          then

          consider M,N be strict feasible MSAlgebra over S, f be ManySortedFunction of M, N such that

           A3: M = o19 and

           A4: N = o29 and f = t and

           A5: the Sorts of M is_transformable_to the Sorts of N and

           A6: f is_homomorphism (M,N) by Def3;

          set s = the Element of ( MSAlg_morph (S,A,o29,o39));

          ( MSAlg_morph (S,A,o29,o39)) <> {} by A2, Def4;

          then

          consider M1,N1 be strict feasible MSAlgebra over S, g be ManySortedFunction of M1, N1 such that

           A7: M1 = o29 and

           A8: N1 = o39 and g = s and

           A9: the Sorts of M1 is_transformable_to the Sorts of N1 and

           A10: g is_homomorphism (M1,N1) by Def3;

          reconsider g9 = g as ManySortedFunction of N, N1 by A4, A7;

          consider GF be ManySortedFunction of M, N1 such that GF = (g9 ** f) and

           A11: GF is_homomorphism (M,N1) by A4, A5, A6, A7, A9, A10, Th5;

          the Sorts of M is_transformable_to the Sorts of N1 by A4, A5, A7, A9, AUTALG_1: 10;

          then GF in ( MSAlg_morph (S,A,o19,o39)) by A3, A8, A11, Def3;

          hence thesis by Def4;

        end;

        thus C is associative

        proof

          let i,j,k,l be Element of M;

          let f,g,h be set;

          reconsider i9 = i, j9 = j, k9 = k, l9 = l as Element of ( MSAlg_set (S,A)) by Def4;

          assume that

           A12: f in (GM . (i,j)) and

           A13: g in (GM . (j,k)) and

           A14: h in (GM . (k,l));

          g in ( MSAlg_morph (S,A,j9,k9)) by A13, Def4;

          then

          consider M2,N2 be strict feasible MSAlgebra over S, G be ManySortedFunction of M2, N2 such that

           A15: M2 = j9 and

           A16: N2 = k9 and

           A17: g = G and

           A18: the Sorts of M2 is_transformable_to the Sorts of N2 and

           A19: G is_homomorphism (M2,N2) by Def3;

          h in ( MSAlg_morph (S,A,k9,l9)) by A14, Def4;

          then

          consider M3,N3 be strict feasible MSAlgebra over S, H be ManySortedFunction of M3, N3 such that

           A20: M3 = k9 and

           A21: N3 = l9 and

           A22: h = H and

           A23: the Sorts of M3 is_transformable_to the Sorts of N3 and

           A24: H is_homomorphism (M3,N3) by Def3;

          reconsider G9 = G as ManySortedFunction of M2, M3 by A16, A20;

          consider HG be ManySortedFunction of M2, N3 such that

           A25: HG = (H ** G9) and

           A26: HG is_homomorphism (M2,N3) by A16, A18, A19, A20, A23, A24, Th5;

          

           A27: ((C . (j,k,l)) . (H,G)) = (H ** G9) by A13, A14, A17, A22, Def4;

          f in ( MSAlg_morph (S,A,i9,j9)) by A12, Def4;

          then

          consider M1,N1 be strict feasible MSAlgebra over S, F be ManySortedFunction of M1, N1 such that

           A28: M1 = i9 and

           A29: N1 = j9 and

           A30: f = F and

           A31: the Sorts of M1 is_transformable_to the Sorts of N1 and

           A32: F is_homomorphism (M1,N1) by Def3;

          

           A33: ((C . (i,j,k)) . (g,f)) = (G ** F) by A12, A13, A30, A17, Def4;

          consider GF be ManySortedFunction of M1, M3 such that

           A34: GF = (G9 ** F) and

           A35: GF is_homomorphism (M1,M3) by A29, A31, A32, A15, A16, A18, A19, A20, Th5;

          the Sorts of M1 is_transformable_to the Sorts of M3 by A29, A31, A15, A16, A18, A20, AUTALG_1: 10;

          then (G9 ** F) in ( MSAlg_morph (S,A,i9,k9)) by A28, A20, A34, A35, Def3;

          then GF in (GM . (i,k)) by A34, Def4;

          then

           A36: ((C . (i,k,l)) . (H,GF)) = (H ** GF) by A14, A22, Def4;

          the Sorts of M2 is_transformable_to the Sorts of N3 by A16, A18, A20, A23, AUTALG_1: 10;

          then HG in ( MSAlg_morph (S,A,j9,l9)) by A15, A21, A26, Def3;

          then

           A37: (H ** G9) in (GM . (j,l)) by A25, Def4;

          ((H ** G9) ** F) = (H ** (G9 ** F)) by PBOOLE: 140;

          hence thesis by A12, A30, A17, A22, A33, A34, A36, A27, A37, Def4;

        end;

        thus C is with_left_units

        proof

          let j be Element of M;

          reconsider j9 = j as Element of ( MSAlg_set (S,A)) by Def4;

          consider MS be strict feasible MSAlgebra over S such that

           A38: MS = j9 and for C be Component of the Sorts of MS holds C c= A by Def2;

          reconsider e = ( id the Sorts of MS) as ManySortedFunction of MS, MS;

          take e;

          e is_homomorphism (MS,MS) & (GM . (j,j)) = ( MSAlg_morph (S,A,j9,j9)) by Def4, MSUALG_3: 9;

          hence

           A39: e in (GM . (j,j)) by A38, Def3;

          let i be Element of M;

          reconsider i9 = i as Element of ( MSAlg_set (S,A)) by Def4;

          let f be set;

          reconsider I = i, J = j as Object of M;

          assume

           A40: f in (GM . (i,j));

          then f in ( MSAlg_morph (S,A,i9,j9)) by Def4;

          then

          consider M1,N1 be strict feasible MSAlgebra over S, F be ManySortedFunction of M1, N1 such that M1 = i9 and

           A41: N1 = j9 and

           A42: F = f and the Sorts of M1 is_transformable_to the Sorts of N1 and F is_homomorphism (M1,N1) by Def3;

          reconsider F as ManySortedFunction of M1, MS by A38, A41;

          ((C . (I,J,J)) . (e,f)) = (e ** F) by A39, A40, A42, Def4;

          hence thesis by A42, MSUALG_3: 4;

        end;

        thus C is with_right_units

        proof

          let i be Element of M;

          reconsider i9 = i as Element of ( MSAlg_set (S,A)) by Def4;

          consider MS be strict feasible MSAlgebra over S such that

           A43: MS = i9 and for C be Component of the Sorts of MS holds C c= A by Def2;

          reconsider e = ( id the Sorts of MS) as ManySortedFunction of MS, MS;

          take e;

          e is_homomorphism (MS,MS) & (GM . (i,i)) = ( MSAlg_morph (S,A,i9,i9)) by Def4, MSUALG_3: 9;

          hence

           A44: e in (GM . (i,i)) by A43, Def3;

          let j be Element of M;

          reconsider j9 = j as Element of ( MSAlg_set (S,A)) by Def4;

          let f be set;

          reconsider I = i, J = j as Object of M;

          assume

           A45: f in (GM . (i,j));

          then f in ( MSAlg_morph (S,A,i9,j9)) by Def4;

          then

          consider M1,N1 be strict feasible MSAlgebra over S, F be ManySortedFunction of M1, N1 such that

           A46: M1 = i9 and N1 = j9 and

           A47: F = f and the Sorts of M1 is_transformable_to the Sorts of N1 and F is_homomorphism (M1,N1) by Def3;

          reconsider F as ManySortedFunction of MS, N1 by A43, A46;

          ((C . (I,I,J)) . (f,e)) = (F ** e) by A44, A45, A47, Def4;

          hence thesis by A47, MSUALG_3: 3;

        end;

      end;

    end

    theorem :: MSINST_1:6

    for C be category st C = ( MSAlgCat (S,A)) holds for o be Object of C holds o is strict feasible MSAlgebra over S

    proof

      let C be category such that

       A1: C = ( MSAlgCat (S,A));

      let o be Object of C;

      o in the carrier of C;

      then o in ( MSAlg_set (S,A)) by A1, Def4;

      then ex M be strict feasible MSAlgebra over S st o = M & for C1 be Component of the Sorts of M holds C1 c= A by Def2;

      hence thesis;

    end;