:: Algebra of Morphisms
::  by Grzegorz Bancerek
::
:: Received January 28, 1997
:: Copyright (c) 1997-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies FUNCT_1, PBOOLE, RELAT_1, FUNCOP_1, CARD_3, TARSKI, FUNCT_6,
      MEMBER_1, XBOOLE_0, FINSEQ_1, MSUALG_1, STRUCT_0, PROB_2, MSAFREE,
      ZFMISC_1, CARD_1, FINSEQ_2, MCART_1, SUBSET_1, ORDINAL4, MSUALG_6, CAT_5,
      INSTALG1, NUMBERS, MARGREL1, CAT_1, PUA2MSS1, GRAPH_1, PARTFUN1,
      MSUALG_3, CATALG_1, MONOID_0;
 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1,
      XTUPLE_0, SUBSET_1, NUMBERS, MCART_1,
      RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, MSAFREE1,
      FINSEQ_1, FINSEQ_2, CARD_3, FINSEQ_4, FUNCT_6, STRUCT_0, PBOOLE,
      MSUALG_1, MSUALG_3, MSAFREE, PUA2MSS1, MSUALG_6, INSTALG1, GRAPH_1,
      CAT_1;
 constructors ENUMSET1, FINSEQ_4, CAT_1, MSUALG_3, MSAFREE1, PUA2MSS1,
      MSUALG_6, INSTALG1, RELSET_1, XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2,
      FUNCOP_1, FINSEQ_1, FINSEQ_2, STRUCT_0, MSUALG_1, RELSET_1, MSAFREE,
      INSTALG1, MSAFREE1, MSSUBFAM, PBOOLE, XTUPLE_0;
 requirements NUMERALS, BOOLE, SUBSET;
 definitions TARSKI, STRUCT_0, MSUALG_1, MSUALG_3, PUA2MSS1, MSUALG_6,
      INSTALG1, PROB_2, MSAFREE1, XBOOLE_0, FUNCOP_1, PBOOLE, CAT_1, XTUPLE_0;
 theorems TARSKI, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2,
      FINSEQ_3, FUNCT_3, MCART_1, ENUMSET1, FUNCT_6, FINSEQ_4, MONOID_1,
      CARD_3, PBOOLE, PRALG_2, MSUALG_3, INSTALG1, CAT_1, RELSET_1, XBOOLE_0,
      XBOOLE_1, FUNCOP_1, PARTFUN1, CARD_1, XTUPLE_0;
 schemes FUNCT_1, CLASSES1, PBOOLE, XBOOLE_0;

begin :: Preliminaries

definition
  let I be set;
  let A,f be Function;
  func f-MSF(I,A) -> ManySortedFunction of I means
  : Def1:
  for i being set st i in I holds it.i = f|(A.i);
  existence
  proof
    deffunc f(set) = f|(A.$1);
    consider F being ManySortedSet of I such that
A1: for i being set st i in I holds F.i = f(i) from PBOOLE:sch 4;
    F is Function-yielding
    proof
      let x be set;
      assume x in dom F;
      then x in I;
      then F.x = f|(A.x) by A1;
      hence thesis;
    end;
    hence thesis by A1;
  end;
  uniqueness
  proof
    let g1,g2 be ManySortedFunction of I such that
A2: for i being set st i in I holds g1.i = f|(A.i) and
A3: for i being set st i in I holds g2.i = f|(A.i);
    now
      let i be set;
      assume
A4:   i in I;
      then g1.i = f|(A.i) by A2;
      hence g1.i = g2.i by A3,A4;
    end;
    hence thesis by PBOOLE:3;
  end;
end;

theorem
  for I being set, A being ManySortedSet of I holds (id Union A)-MSF(I,A
  ) = id A
proof
  let I be set, A be ManySortedSet of I;
  set f = id Union A, F = f-MSF(I,A);
  now
    let i be set;
A1: Union A = union rng A by CARD_3:def 4;
    assume
A2: i in I;
    then i in dom A by PARTFUN1:def 2;
    then
A3: A.i in rng A by FUNCT_1:def 3;
    F.i = f|(A.i) & (id A).i = id (A.i) by A2,Def1,MSUALG_3:def 1;
    hence F.i = (id A).i by A3,A1,FUNCT_3:1,ZFMISC_1:74;
  end;
  hence thesis by PBOOLE:3;
end;

theorem
  for I being set, A,B being ManySortedSet of I for f,g being Function
  st rngs (f-MSF(I,A)) c= B holds (g*f)-MSF(I,A) = (g-MSF(I,B))**(f-MSF(I,A))
proof
  let I be set, A,B be ManySortedSet of I;
  let f,g be Function such that
A1: rngs (f-MSF(I,A)) c= B;
A2: I /\ I = I;
  dom (g-MSF(I,B)) = I & dom (f-MSF(I,A)) = I by PARTFUN1:def 2;
  then
A3: dom ((g-MSF(I,B))**(f-MSF(I,A))) = I by A2,PBOOLE:def 19;
A4: now
    let i be set;
    assume
A5: i in I;
    then
A6: (f-MSF(I,A)).i = f|(A.i) by Def1;
    dom (f-MSF(I,A)) = I by PARTFUN1:def 2;
    then (rngs (f-MSF(I,A))).i = rng (f|(A.i)) by A5,A6,FUNCT_6:22;
    then rng (f|(A.i)) c= B.i by A1,A5,PBOOLE:def 2;
    then (g*f)|(A.i) = g*(f|(A.i)) & (B.i)|`(f|(A.i)) = f|(A.i)
      by RELAT_1:83,94;
    then
A7: (g*f)|(A.i) = (g|(B.i))*(f|(A.i)) by MONOID_1:1;
    ((g*f)-MSF(I,A)).i = (g*f)|(A.i) & (g-MSF(I,B)).i = g|(B.i) by A5,Def1;
    hence ((g*f)-MSF(I,A)).i = ((g-MSF(I,B))**(f-MSF(I,A))).i by A3,A5,A6,A7,
PBOOLE:def 19;
  end;
  dom ((g*f)-MSF(I,A)) = I by PARTFUN1:def 2;
  hence thesis by A3,A4,FUNCT_1:2;
end;

theorem
  for f being Function, I being set for A,B being ManySortedSet of I st
for i being set st i in I holds A.i c= dom f & f.:(A.i) c= B.i holds f-MSF(I,A)
  is ManySortedFunction of A,B
proof
  let f be Function, I be set;
  let A,B be ManySortedSet of I such that
A1: for i being set st i in I holds A.i c= dom f & f.:(A.i) c= B.i;
  let i be set;
  assume
A2: i in I;
  then
A3: (f-MSF(I,A)).i = f|(A.i) by Def1;
  f.:(A.i) c= B.i by A1,A2;
  then
A4: rng ((f-MSF(I,A)).i) c= B.i by A3,RELAT_1:115;
  dom ((f-MSF(I,A)).i) = A.i by A1,A2,A3,RELAT_1:62;
  hence thesis by A4,FUNCT_2:2;
end;

Lm1: now
  let x,y be set;
  assume <*x*> = <*y*>;
  then <*x*>.1 = y by FINSEQ_1:40;
  hence x = y by FINSEQ_1:40;
end;

definition
  let S be non empty ManySortedSign;
  let A be MSAlgebra over S;

  attr A is empty means
  : Def2:
  the Sorts of A is empty-yielding;
end;

registration
  let S be non empty ManySortedSign;
  cluster non-empty -> non empty for MSAlgebra over S;
  coherence
  proof
    let A be MSAlgebra over S;
    assume the Sorts of A is non-empty;
    hence the Sorts of A is not empty-yielding;
  end;
end;

registration
  let S be non empty non void ManySortedSign;
  cluster strict non-empty disjoint_valued for MSAlgebra over S;
  existence
  proof
    set X = the non-empty ManySortedSet of the carrier of S;
    take FreeMSA X;
    thus thesis;
  end;
end;

registration
  let S be non empty non void ManySortedSign;
  let A be non empty MSAlgebra over S;
  cluster the Sorts of A -> non empty-yielding;
  coherence by Def2;
end;

registration
  cluster non empty-yielding for Function;
  existence
  proof
    set S = the non empty non void ManySortedSign;
    set A = the non empty MSAlgebra over S;
    take the Sorts of A;
    thus thesis;
  end;
end;

begin :: Signature of a category

definition
  let A be set;

  func CatSign A -> strict ManySortedSign means
  : Def3:
  the carrier of it = [:
  {0},2-tuples_on A:] & the carrier' of it = [:{1},1-tuples_on A:] \/ [:{2},3
-tuples_on A:] & (for a being set st a in A holds (the Arity of it).[1,<*a*>] =
{} & (the ResultSort of it).[1,<*a*>] = [0,<*a,a*>]) & for a,b,c being set st a
in A & b in A & c in A holds (the Arity of it).[2,<*a,b,c*>] = <*[0,<*b,c*>],[0
  ,<*a,b*>]*> & (the ResultSort of it).[2,<*a,b,c*>] = [0,<*a,c*>];
  existence
  proof
    defpred R[set,set] means ex y1,y2,y3 being set st y1 in A & y2 in A & y3
in A & ($1 = [1,<*y1*>] & $2 = [0,<*y1,y1*>] or $1 = [2,<*y1,y2,y3*>] & $2 = [0
    ,<*y1,y3*>]);
    defpred P[set,set] means ex y1,y2,y3 being set st y1 in A & y2 in A & y3
in A & ($1 = [1,<*y1*>] & $2 = {} or $1 = [2,<*y1,y2,y3*>] & $2 = <*[0,<*y2,y3
    *>],[0,<*y1,y2*>]*>);
A1: for x being set st x in [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A:]
    ex y being set st y in [:{0},2-tuples_on A:]* & P[x,y]
    proof
      let x be set;
      assume
A2:   x in [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A:];
      per cases by A2,XBOOLE_0:def 3;
      suppose
A3:     x in [:{1},1-tuples_on A:];
        then x`2 in 1-tuples_on A by MCART_1:10;
        then
A4:     x`2 in {s where s is Element of A*: len s = 1} by FINSEQ_2:def 4;
        take y = {};
        thus y in [:{0},2-tuples_on A:]* by FINSEQ_1:49;
        consider s being Element of A* such that
A5:     x`2 = s and
A6:     len s = 1 by A4;
        take y1 = s.1, y2 = s.1, y3 = s.1;
A7:     s = <*y1*> by A6,FINSEQ_1:40;
        then y1 in {y1} & rng s = {y1} by FINSEQ_1:39,TARSKI:def 1;
        hence y1 in A & y2 in A & y3 in A;
        x`1 in {1} by A3,MCART_1:10;
        then x`1 = 1 by TARSKI:def 1;
        hence thesis by A3,A5,A7,MCART_1:21;
      end;
      suppose
A8:     x in [:{2},3-tuples_on A:];
        then x`2 in 3-tuples_on A by MCART_1:10;
        then x`2 in {s where s is Element of A*: len s = 3} by FINSEQ_2:def 4;
        then consider s being Element of A* such that
A9:     x`2 = s and
A10:    len s = 3;
        set y1 = s.1, y2 = s.2, y3 = s.3;
A11:    s = <*y1,y2,y3*> by A10,FINSEQ_1:45;
        then
A12:    rng s = {y1,y2,y3} by FINSEQ_2:128;
        then reconsider B = A as non empty set;
        take y = <*[0,<*y2,y3*>],[0,<*y1,y2*>]*>;
A13:    y2 in {y1,y2,y3} by ENUMSET1:def 1;
A14:    y1 in {y1,y2,y3} by ENUMSET1:def 1;
        then
A15:    0 in {0} & <*y1,y2*> in 2-tuples_on B by A13,A12,FINSEQ_2:101
,TARSKI:def 1;
A16:    y3 in {y1,y2,y3} by ENUMSET1:def 1;
        then <*y2,y3*> in 2-tuples_on B by A13,A12,FINSEQ_2:101;
        then reconsider
        z1 = [0,<*y2,y3*>], z2 = [0,<*y1,y2*>] as Element of [:{0},
        2-tuples_on B:] by A15,ZFMISC_1:87;
        y = <*z1*>^<*z2*> by FINSEQ_1:def 9;
        hence y in [:{0},2-tuples_on A:]* by FINSEQ_1:def 11;
        take y1, y2, y3;
        thus y1 in A & y2 in A & y3 in A by A14,A13,A16,A12;
        x`1 in {2} by A8,MCART_1:10;
        then x`1 = 2 by TARSKI:def 1;
        hence thesis by A8,A9,A11,MCART_1:21;
      end;
    end;
    consider Ar being Function such that
A17: dom Ar = [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A:] & rng Ar
    c= [:{0},2 -tuples_on A:]* and
A18: for x being set st x in [:{1},1-tuples_on A:] \/ [:{2},3
    -tuples_on A:] holds P[x,Ar.x] from FUNCT_1:sch 5(A1);
    reconsider Ar as Function of [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A
    :], [:{0},2-tuples_on A:]* by A17,FUNCT_2:2;
A19: for x being set st x in [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A
    :] ex y being set st y in [:{0},2-tuples_on A:] & R[x,y]
    proof
      let x be set;
      assume
A20:  x in [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A:];
      per cases by A20,XBOOLE_0:def 3;
      suppose
A21:    x in [:{1},1-tuples_on A:];
        then x`2 in 1-tuples_on A by MCART_1:10;
        then x`2 in {s where s is Element of A*: len s = 1} by FINSEQ_2:def 4;
        then consider s being Element of A* such that
A22:    x`2 = s and
A23:    len s = 1;
        set y1 = s.1, y2 = s.1, y3 = s.1;
A24:    s = <*y1*> by A23,FINSEQ_1:40;
        then
A25:    y1 in {y1} & rng s = {y1} by FINSEQ_1:39,TARSKI:def 1;
        take y = [0,<*y1,y1*>];
        reconsider B = A as non empty set by A24;
        reconsider y1 as Element of B by A25;
        0 in {0} & <*y1,y1*> in 2-tuples_on B by FINSEQ_2:101,TARSKI:def 1;
        hence y in [:{0},2-tuples_on A:] by ZFMISC_1:87;
        take y1, y2, y3;
        thus y1 in A & y2 in A & y3 in A by A25;
        x`1 in {1} by A21,MCART_1:10;
        then x`1 = 1 by TARSKI:def 1;
        hence x = [1,<*y1*>] & y = [0,<*y1,y1*>] or x = [2,<*y1,y2,y3*>] & y =
        [0,<*y1,y3*>] by A21,A22,A24,MCART_1:21;
      end;
      suppose
A26:    x in [:{2},3-tuples_on A:];
        then x`2 in 3-tuples_on A by MCART_1:10;
        then x`2 in {s where s is Element of A*: len s = 3} by FINSEQ_2:def 4;
        then consider s being Element of A* such that
A27:    x`2 = s and
A28:    len s = 3;
        set y1 = s.1, y2 = s.2, y3 = s.3;
A29:    s = <*y1,y2,y3*> by A28,FINSEQ_1:45;
        then
A30:    rng s = {y1,y2,y3} by FINSEQ_2:128;
        then reconsider B = A as non empty set;
        take y = [0,<*y1,y3*>];
A31:    y1 in {y1,y2,y3} & y3 in {y1,y2,y3} by ENUMSET1:def 1;
        then 0 in {0} & <*y1,y3*> in 2-tuples_on B by A30,FINSEQ_2:101
,TARSKI:def 1;
        hence y in [:{0},2-tuples_on A:] by ZFMISC_1:87;
        take y1, y2, y3;
        y2 in {y1,y2,y3} by ENUMSET1:def 1;
        hence y1 in A & y2 in A & y3 in A by A31,A30;
        x`1 in {2} by A26,MCART_1:10;
        then x`1 = 2 by TARSKI:def 1;
        hence thesis by A26,A27,A29,MCART_1:21;
      end;
    end;
    consider R being Function such that
A32: dom R = [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A:] & rng R c=
    [:{0},2 -tuples_on A:] and
A33: for x being set st x in [:{1},1-tuples_on A:] \/ [:{2},3
    -tuples_on A:] holds R[x,R.x] from FUNCT_1:sch 5(A19);
    reconsider R as Function of [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A:]
    , [:{0},2-tuples_on A:] by A32,FUNCT_2:2;
    take S = ManySortedSign (#[:{0},2-tuples_on A:], [:{1},1-tuples_on A:]\/[:
      {2},3-tuples_on A:], Ar, R#);
    thus the carrier of S = [:{0},2-tuples_on A:];
    thus the carrier' of S = [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A:];
    hereby
      let a be set;
      assume
A34:  a in A;
      then reconsider B = A as non empty set;
      reconsider x = a as Element of B by A34;
      <*x*> is Element of 1-tuples_on B & 1 in {1} by FINSEQ_2:98,TARSKI:def 1
;
      then [1,<*a*>] in [:{1},1-tuples_on A:] by ZFMISC_1:87;
      then
A35:  [1,<*a*>] in [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A:] by
XBOOLE_0:def 3;
      then consider y1,y2,y3 being set such that
      y1 in A and
      y2 in A and
      y3 in A and
A36:  [1,<*a*>] = [1,<*y1*>] & R.[1,<*a*>] = [0,<*y1,y1*>] or [1,<*a
      *>] = [2,<*y1,y2,y3*>] & R.[1,<*a*>] = [0,<*y1,y3*>] by A33;
      ex y1,y2,y3 being set st y1 in A & y2 in A & y3 in A & ([1,<*a*>] =
[1, <*y1*>] & Ar.[1,<*a*>] = {} or [1,<*a*>] = [2,<*y1,y2,y3*>] & Ar.[1,<*a*>]
      = <* [0,<*y2,y3*>],[0,<*y1,y2*>]*>) by A18,A35;
      hence (the Arity of S).[1,<*a*>] = {} by XTUPLE_0:1;
A37:  <*a*>.1 = a & <*y1*>.1 = y1 by FINSEQ_1:40;
      <*a*> = <*y1*> by A36,XTUPLE_0:1;
      hence (the ResultSort of S).[1,<*a*>] = [0,<*a,a*>] by A36,A37,XTUPLE_0:1
;
    end;
    let a,b,c be set;
    assume that
A38: a in A and
A39: b in A & c in A;
    reconsider B = A as non empty set by A38;
    reconsider x = a, y = b, z = c as Element of B by A38,A39;
    <*x,y,z*> is Element of 3-tuples_on B & 2 in {2} by FINSEQ_2:104
,TARSKI:def 1;
    then [2,<*a,b,c*>] in [:{2},3-tuples_on A:] by ZFMISC_1:87;
    then
A40: [2,<*a,b,c*>] in [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A:] by
XBOOLE_0:def 3;
    then consider y1,y2,y3 being set such that
    y1 in A and
    y2 in A and
    y3 in A and
A41: [2,<*a,b,c*>] = [1,<*y1*>] & Ar.[2,<*a,b,c*>] = {} or [2,<*a,b,c
*>] = [2,<*y1,y2,y3*>] & Ar.[2,<*a,b,c*>] = <*[0,<*y2,y3*>],[0,<*y1,y2*>]*> by
A18;
A42: <*a,b,c*> = <*a*>^<*b*>^<*c*> & <*y1,y2,y3*> = <*y1*>^<*y2*>^<*y3*>
    by FINSEQ_1:def 10;
A43: <*a,b,c*> = <*y1,y2,y3*> by A41,XTUPLE_0:1;
    then
A44: <*a*>^<*b*> = <*y1*>^<*y2*> by A42,FINSEQ_2:17;
    then <*a*> = <*y1*> by FINSEQ_2:17;
    then
A45: a = y1 by Lm1;
    b = y2 by A44,FINSEQ_2:17;
    hence
    (the Arity of S).[2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> by A41,A43,A42
,A45,FINSEQ_2:17,XTUPLE_0:1;
    consider y1,y2,y3 being set such that
    y1 in A and
    y2 in A and
    y3 in A and
A46: [2,<*a,b,c*>] = [1,<*y1*>] & R.[2,<*a,b,c*>] = [0,<*y1,y1*>] or [
2,<*a,b,c*>] = [2,<*y1,y2,y3*>] & R.[2,<*a,b,c*>] = [0,<*y1,y3*>] by A33,A40;
A47: <*a,b,c*>.1 = a & <*y1,y2,y3*>.1 = y1 by FINSEQ_1:45;
A48: <*a,b,c*>.3 = c by FINSEQ_1:45;
    <*a,b,c*> = <*y1,y2,y3*> by A46,XTUPLE_0:1;
    hence thesis by A46,A47,A48,FINSEQ_1:45,XTUPLE_0:1;
  end;
  correctness
  proof
    let S1,S2 be strict ManySortedSign such that
A49: the carrier of S1 = [:{0},2-tuples_on A:] and
A50: the carrier' of S1 = [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A :] and
A51: for a being set st a in A holds (the Arity of S1).[1,<*a*>] = {}
    & (the ResultSort of S1).[1,<*a*>] = [0,<*a,a*>] and
A52: for a,b,c being set st a in A & b in A & c in A holds (the Arity
of S1).[2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & (the ResultSort of S1).[2,
    <*a,b,c*>] = [0,<*a,c*>] and
A53: the carrier of S2 = [:{0},2-tuples_on A:] and
A54: the carrier' of S2 = [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A :] and
A55: for a being set st a in A holds (the Arity of S2).[1,<*a*>] = {}
    & (the ResultSort of S2).[1,<*a*>] = [0,<*a,a*>] and
A56: for a,b,c being set st a in A & b in A & c in A holds (the Arity
of S2).[2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & (the ResultSort of S2).[2,
    <*a,b,c*>] = [0,<*a,c*>];
A57: now
      let x be set;
      assume x in [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A:];
      then
A58:  x in [:{1},1-tuples_on A:] or x in [:{2},3-tuples_on A:] by
XBOOLE_0:def 3;
      then x`1 in {1} & x`2 in 1-tuples_on A or x`1 in {2} & x`2 in 3
      -tuples_on A by MCART_1:10;
      then
A59:  x`1 = 1 & x`2 in 1-tuples_on A or x`1 = 2 & x`2 in 3-tuples_on A by
TARSKI:def 1;
A60:  now
        assume x`2 in 3-tuples_on A;
        then consider a,b,c being set such that
A61:    a in A & b in A & c in A & x`2 = <*a,b,c*> by FINSEQ_2:139;
        thus (the Arity of S1).[2,x`2] = <*[0,<*b,c*>],[0,<*a,b*>]*> by A52,A61
          .= (the Arity of S2).[2,x`2] by A56,A61;
      end;
A62:  now
        assume x`2 in 1-tuples_on A;
        then
A63:    ex a being set st a in A & x`2 = <*a*> by FINSEQ_2:135;
        hence (the Arity of S1).[1,x`2] = {} by A51
          .= (the Arity of S2).[1,x`2] by A55,A63;
      end;
      x = [x`1,x`2] by A58,MCART_1:21;
      hence (the Arity of S1).x = (the Arity of S2).x by A59,A62,A60;
    end;
A64: now
      let x be set;
      assume x in [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A:];
      then
A65:  x in [:{1},1-tuples_on A:] or x in [:{2},3-tuples_on A:] by
XBOOLE_0:def 3;
      then x`1 in {1} & x`2 in 1-tuples_on A or x`1 in {2} & x`2 in 3
      -tuples_on A by MCART_1:10;
      then
A66:  x`1 = 1 & x`2 in 1-tuples_on A or x`1 = 2 & x`2 in 3-tuples_on A
      by TARSKI:def 1;
A67:  now
        assume x`2 in 3-tuples_on A;
        then consider a,b,c being set such that
A68:    a in A & b in A & c in A & x`2 = <*a,b,c*> by FINSEQ_2:139;
        thus (the ResultSort of S1).[2,x`2] = [0,<*a,c*>] by A52,A68
          .= (the ResultSort of S2).[2,x`2] by A56,A68;
      end;
A69:  now
        assume x`2 in 1-tuples_on A;
        then consider a being set such that
A70:    a in A & x`2 = <*a*> by FINSEQ_2:135;
        thus (the ResultSort of S1).[1,x`2] = [0,<*a,a*>] by A51,A70
          .= (the ResultSort of S2).[1,x`2] by A55,A70;
      end;
      x = [x`1,x`2] by A65,MCART_1:21;
      hence (the ResultSort of S1).x = (the ResultSort of S2).x by A66,A69,A67;
    end;
    dom the Arity of S1 = the carrier' of S1 & dom the Arity of S2 = the
    carrier' of S2 by FUNCT_2:def 1;
    then
A71: the Arity of S1 = the Arity of S2 by A50,A54,A57,FUNCT_1:2;
    now
      assume [:{0},2-tuples_on A:] = {};
      then A = {};
      then
A72:  1 <> 0 & 3 <> 0 implies 1-tuples_on A = {} & 3-tuples_on A = {} by
FINSEQ_3:119;
      then [:{1},1-tuples_on A:] = {} by ZFMISC_1:90;
      hence [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A:] = {} by A72,
ZFMISC_1:90;
    end;
    then dom the ResultSort of S1 = the carrier' of S1 & dom the ResultSort
    of S2 = the carrier' of S2 by A49,A50,A53,A54,FUNCT_2:def 1;
    hence thesis by A49,A50,A53,A54,A71,A64,FUNCT_1:2;
  end;
end;

registration
  let A be set;
  cluster CatSign A -> feasible;
  coherence
  proof
    assume the carrier of CatSign A = {};
    then [:{0},2-tuples_on A:] = {} by Def3;
    then A = {};
    then
A1: 1 <> 0 & 3 <> 0 implies 1-tuples_on A = {} & 3-tuples_on A = {} by
FINSEQ_3:119;
    then [:{1},1-tuples_on A:] = {} by ZFMISC_1:90;
    then [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A:] = {} by A1,ZFMISC_1:90
;
    hence thesis by Def3;
  end;
end;

registration
  let A be non empty set;
  cluster CatSign A -> non empty non void;
  coherence
  proof
    the carrier of CatSign A = [:{0},2-tuples_on A:] by Def3;
    hence the carrier of CatSign A is non empty;
    the carrier' of CatSign A = [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on
    A:] by Def3;
    hence the carrier' of CatSign A is non empty;
  end;
end;

definition
  mode Signature is feasible ManySortedSign;
end;

definition
  let S be Signature;
  attr S is Categorial means
  : Def4:
  ex A being set st CatSign A is
  Subsignature of S & the carrier of S = [:{0},2-tuples_on A:];
end;

registration
  cluster Categorial -> non void for non empty Signature;
  coherence
  proof
    let S be non empty Signature;
    given A being set such that
A1: CatSign A is Subsignature of S and
A2: the carrier of S = [:{0},2-tuples_on A:];
    set s = the SortSymbol of S;
    consider z,p being set such that
    z in {0} and
A3: p in 2-tuples_on A and
    s = [z,p] by A2,ZFMISC_1:84;
    2-tuples_on A = {q where q is Element of A*: len q = 2} by FINSEQ_2:def 4;
    then consider q being Element of A* such that
    p = q and
A4: len q = 2 by A3;
A5: dom q = Seg 2 by A4,FINSEQ_1:def 3;
    then reconsider A9 = A as non empty set;
    1 in dom q by A5,FINSEQ_1:2,TARSKI:def 2;
    then q.1 in rng q by FUNCT_1:def 3;
    then reconsider a = q.1 as Element of A9;
    the carrier' of CatSign A = [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on
    A :] by Def3;
    then
    <*a*> is Element of 1-tuples_on A9 & [:{1},1-tuples_on A:] \/ [:{2},3
    -tuples_on A:] c= the carrier' of S by A1,FINSEQ_2:98,INSTALG1:10;
    hence the carrier' of S is non empty;
  end;
end;

registration
  cluster Categorial non empty strict for Signature;
  existence
  proof
    take S = CatSign {{}};
    thus S is Categorial
    proof
      take {{}};
      thus thesis by Def3,INSTALG1:15;
    end;
    thus thesis;
  end;
end;

definition
  mode CatSignature is Categorial Signature;
end;

definition
  let A be set;
  mode CatSignature of A -> Signature means
    : Def5:
    CatSign A is Subsignature
    of it & the carrier of it = [:{0},2-tuples_on A:];
  existence
  proof
    set S = CatSign A;
    S is Subsignature of S & the carrier of S = [:{0},2-tuples_on A:] by Def3,
INSTALG1:15;
    then reconsider S as CatSignature by Def4;
    take S;
    thus thesis by Def3,INSTALG1:15;
  end;
end;

theorem
  for A1,A2 being set, S being CatSignature of A1 st S is CatSignature
  of A2 holds A1 = A2
proof
  let A1,A2 be set, S be CatSignature of A1;
  assume that
  CatSign A2 is Subsignature of S and
A1: the carrier of S = [:{0},2-tuples_on A2:];
A2: [:{0},2-tuples_on A1:] = [:{0},2-tuples_on A2:] by A1,Def5;
  then
A3: 2-tuples_on A1 c= 2-tuples_on A2 by ZFMISC_1:94;
  hereby
    let x be set;
    assume x in A1;
    then <*x,x*> in 2-tuples_on A1 by FINSEQ_2:137;
    hence x in A2 by A3,FINSEQ_2:138;
  end;
  let x be set;
  assume x in A2;
  then
A4: <*x,x*> in 2-tuples_on A2 by FINSEQ_2:137;
  2-tuples_on A2 c= 2-tuples_on A1 by A2,ZFMISC_1:94;
  hence thesis by A4,FINSEQ_2:138;
end;

registration
  let A be set;
  cluster -> Categorial for CatSignature of A;
  coherence
  proof
    let S be CatSignature of A;
    take A;
    thus thesis by Def5;
  end;
end;

registration
  let A be non empty set;
  cluster -> non empty for CatSignature of A;
  coherence
  proof

    let S be CatSignature of A;
    CatSign A is Subsignature of S by Def5;
    then the carrier of CatSign A c= the carrier of S by INSTALG1:10;
    hence the carrier of S is not empty;
  end;
end;

registration
  let A be set;
  cluster strict for CatSignature of A;
  existence
  proof
    set S = CatSign A;
    S is Subsignature of S & the carrier of S = [:{0},2-tuples_on A:] by Def3,
INSTALG1:15;
    then S is CatSignature of A by Def5;
    hence thesis;
  end;
end;

definition
  let A be set;
  redefine func CatSign A -> strict CatSignature of A;
  coherence
  proof
    set S = CatSign A;
    S is Subsignature of S & the carrier of S = [:{0}, 2-tuples_on A:] by Def3,
INSTALG1:15;
    hence thesis by Def5;
  end;
end;

definition
  let S be ManySortedSign;
  func underlay S means
  : Def6:
  for x being set holds x in it iff ex a being
set, f being Function st [a,f] in (the carrier of S) \/ (the carrier' of S) & x
  in rng f;
  existence
  proof
    set A = (the carrier of S) \/ (the carrier' of S);
    take X = proj2 union SubFuncs proj2 A;
    let x be set;
    hereby
      assume x in X;
      then consider a being set such that
A1:   [a,x] in union SubFuncs proj2 A by XTUPLE_0:def 13;
      consider b being set such that
A2:   [a,x] in b and
A3:   b in SubFuncs proj2 A by A1,TARSKI:def 4;
      reconsider b as Function by A3,FUNCT_6:def 1;
      b in proj2 A by A3,FUNCT_6:def 1;
      then consider c being set such that
A4:   [c,b] in A by XTUPLE_0:def 13;
      take c,b;
      thus [c,b] in A & x in rng b by A2,A4,XTUPLE_0:def 13;
    end;
    given a being set, f being Function such that
A5: [a,f] in (the carrier of S) \/ (the carrier' of S) and
A6: x in rng f;
    consider b being set such that
A7: [b,x] in f by A6,XTUPLE_0:def 13;
    f in proj2 A by A5,XTUPLE_0:def 13;
    then f in SubFuncs proj2 A by FUNCT_6:def 1;
    then [b,x] in union SubFuncs proj2 A by A7,TARSKI:def 4;
    hence thesis by XTUPLE_0:def 13;
  end;
  uniqueness
  proof
    defpred P[set] means ex a being set, f being Function st [a,f] in (the
    carrier of S) \/ (the carrier' of S) & $1 in rng f;
    thus for X1,X2 being set st (for x being set holds x in X1 iff P[ x]) & (
    for x being set holds x in X2 iff P[ x]) holds X1 = X2 from XBOOLE_0:sch 3;
  end;
end;

theorem Th5:
  for A being set holds underlay CatSign A = A
proof
  let A be set;
  set S = CatSign A;
A1: the carrier' of S = [:{1},1-tuples_on A:] \/ [:{2}, 3-tuples_on A:] by Def3
;
  hereby
    let x be set;
    assume x in underlay CatSign A;
    then consider a being set, f being Function such that
A2: [a,f] in (the carrier of S) \/ (the carrier' of S) and
A3: x in rng f by Def6;
    [a,f] in the carrier of S or [a,f] in the carrier' of S by A2,
XBOOLE_0:def 3;
    then
    [a,f] in [:{0},2-tuples_on A:] or [a,f] in [:{1},1-tuples_on A:] or [a
    ,f] in [:{2},3-tuples_on A:] by A1,Def3,XBOOLE_0:def 3;
    then f in 2-tuples_on A or f in 1-tuples_on A or f in 3-tuples_on A by
ZFMISC_1:87;
    then f is FinSequence of A by FINSEQ_2:def 3;
    then rng f c= A by FINSEQ_1:def 4;
    hence x in A by A3;
  end;
  let x be set;
  assume x in A;
  then
A4: <*x,x*> in 2-tuples_on A by FINSEQ_2:137;
  the carrier of S = [:{0},2-tuples_on A:] by Def3;
  then [0,<*x,x*>] in the carrier of S by A4,ZFMISC_1:105;
  then
A5: [0,<*x,x*>] in (the carrier of S) \/ (the carrier' of S) by XBOOLE_0:def 3;
  rng <*x,x*> = {x,x} by FINSEQ_2:127;
  then x in rng <*x,x*> by TARSKI:def 2;
  hence thesis by A5,Def6;
end;

definition
  let S be ManySortedSign;
  attr S is delta-concrete means
  : Def7:
  ex f being Function of NAT,NAT st (
  for s being set st s in the carrier of S ex i being (Element of NAT), p being
FinSequence st s = [i,p] & len p = f.i & [:{i}, (f.i)-tuples_on underlay S:] c=
  the carrier of S) & (for o being set st o in the carrier' of S ex i being (
Element of NAT), p being FinSequence st o = [i,p] & len p = f.i & [:{i}, (f.i)
  -tuples_on underlay S:] c= the carrier' of S);
end;

registration
  let A be set;
  cluster CatSign A -> delta-concrete;
  coherence
  proof
    defpred P[set,set] means ($1 = 0 implies $2 = 2) & ($1 = 1 implies $2 = 1)
    & ($1 = 2 implies $2 = 3);
    set S = CatSign A;
A1: for x be set st x in NAT ex y be set st y in NAT & P[x,y]
    proof
      reconsider j0 = 2, j1 = 1, j2 = 3 as set;
      let i be set;
      assume i in NAT;
      per cases;
      suppose
A2:     i = 0;
        take j0;
        thus thesis by A2;
      end;
      suppose
A3:     i = 1;
        take j1;
        thus thesis by A3;
      end;
      suppose
A4:     i = 2;
        take j2;
        thus thesis by A4;
      end;
      suppose
A5:     i <> 0 & i <> 1 & i <> 2;
        take j0;
        thus thesis by A5;
      end;
    end;
    consider f being Function such that
A6: dom f = NAT & rng f c= NAT and
A7: for i being set st i in NAT holds P[i,f.i] from FUNCT_1:sch 5(A1);
    reconsider f as Function of NAT,NAT by A6,FUNCT_2:2;
    take f;
A8: A = underlay S by Th5;
A9: the carrier of S = [:{0},2-tuples_on A:] by Def3;
    hereby
      let s be set;
      assume s in the carrier of S;
      then consider i, p being set such that
A10:  i in {0} and
A11:  p in 2-tuples_on A and
A12:  s = [i,p] by A9,ZFMISC_1:84;
      reconsider p as FinSequence by A11;
      take i = 0, p;
      f.i = 2 by A7;
      hence s = [i,p] & len p = f.i by A10,A11,A12,FINSEQ_2:132,TARSKI:def 1;
      thus [:{i}, (f.i)-tuples_on underlay S:] c= the carrier of S by A7,A9,A8;
    end;
    let o be set;
A13: the carrier' of S = [:{1},1-tuples_on A:] \/ [:{2}, 3-tuples_on A:] by
Def3;
    assume
A14: o in the carrier' of S;
    per cases by A13,A14,XBOOLE_0:def 3;
    suppose
      o in [:{1}, 1-tuples_on A:];
      then consider i,p being set such that
A15:  i in {1} and
A16:  p in 1-tuples_on A and
A17:  o = [i,p] by ZFMISC_1:84;
      reconsider p as FinSequence of A by A16,FINSEQ_2:def 3;
      take i = 1, p;
      f.i = 1 by A7;
      hence thesis by A13,A8,A15,A16,A17,FINSEQ_2:132,TARSKI:def 1,XBOOLE_1:7;
    end;
    suppose
      o in [:{2}, 3-tuples_on A:];
      then consider i,p being set such that
A18:  i in {2} and
A19:  p in 3-tuples_on A and
A20:  o = [i,p] by ZFMISC_1:84;
      reconsider p as FinSequence of A by A19,FINSEQ_2:def 3;
      take i = 2, p;
      f.i = 3 by A7;
      hence thesis by A13,A8,A18,A19,A20,FINSEQ_2:132,TARSKI:def 1,XBOOLE_1:7;
    end;
  end;
end;

registration
  cluster delta-concrete non empty strict for CatSignature;
  existence
  proof
    take CatSign {{}};
    thus thesis;
  end;
  let A be set;
  cluster delta-concrete strict for CatSignature of A;
  existence
  proof
    take CatSign A;
    thus thesis;
  end;
end;

theorem Th6:
  for S being delta-concrete ManySortedSign, x being set st x in
the carrier of S or x in the carrier' of S ex i being (Element of NAT), p being
  FinSequence st x = [i,p] & rng p c= underlay S
proof
  let S be delta-concrete ManySortedSign, x be set such that
A1: x in the carrier of S or x in the carrier' of S;
A2: x in (the carrier of S) \/ the carrier' of S by A1,XBOOLE_0:def 3;
  consider f being Function of NAT,NAT such that
A3: for s being set st s in the carrier of S ex i being (Element of NAT)
  , p being FinSequence st s = [i,p] & len p = f.i & [:{i}, (f.i)-tuples_on
  underlay S:] c= the carrier of S and
A4: for o being set st o in the carrier' of S ex i being (Element of NAT
  ), p being FinSequence st o = [i,p] & len p = f.i & [:{i}, (f.i)-tuples_on
  underlay S:] c= the carrier' of S by Def7;
  per cases by A1;
  suppose
    x in the carrier of S;
    then consider i being (Element of NAT), p being FinSequence such that
A5: x = [i,p] and
    len p = f.i and
    [:{i}, (f.i)-tuples_on underlay S:] c= the carrier of S by A3;
    take i,p;
    thus x = [i,p] by A5;
    let a be set;
    thus thesis by A2,A5,Def6;
  end;
  suppose
    x in the carrier' of S;
    then consider i being (Element of NAT), p being FinSequence such that
A6: x = [i,p] and
    len p = f.i and
    [:{i}, (f.i)-tuples_on underlay S:] c= the carrier' of S by A4;
    take i,p;
    thus x = [i,p] by A6;
    let a be set;
    thus thesis by A2,A6,Def6;
  end;
end;

theorem
  for S being delta-concrete ManySortedSign, i being set, p1,p2 being
FinSequence st [i,p1] in the carrier of S & [i,p2] in the carrier of S or [i,p1
  ] in the carrier' of S & [i,p2] in the carrier' of S holds len p1 = len p2
proof
  let S be delta-concrete ManySortedSign, i be set, p1,p2 be FinSequence such
  that
A1: [i,p1] in the carrier of S & [i,p2] in the carrier of S or [i,p1] in
  the carrier' of S & [i,p2] in the carrier' of S;
  consider f being Function of NAT,NAT such that
A2: for s being set st s in the carrier of S ex i being (Element of NAT)
  , p being FinSequence st s = [i,p] & len p = f.i & [:{i}, (f.i)-tuples_on
  underlay S:] c= the carrier of S and
A3: for o being set st o in the carrier' of S ex i being (Element of NAT
  ), p being FinSequence st o = [i,p] & len p = f.i & [:{i}, (f.i)-tuples_on
  underlay S:] c= the carrier' of S by Def7;
  per cases by A1;
  suppose
A4: [i,p1] in the carrier of S & [i,p2] in the carrier of S;
    then consider j1 being (Element of NAT), q1 being FinSequence such that
A5: [i,p1] = [j1,q1] and
A6: len q1 = f.j1 and
    [:{j1}, (f.j1)-tuples_on underlay S:] c= the carrier of S by A2;
A7: i = j1 & p1 = q1 by A5,XTUPLE_0:1;
    consider j2 being (Element of NAT), q2 being FinSequence such that
A8: [i,p2] = [j2,q2] and
A9: len q2 = f.j2 and
    [:{j2}, (f.j2)-tuples_on underlay S:] c= the carrier of S by A2,A4;
    i = j2 by A8,XTUPLE_0:1;
    hence thesis by A6,A8,A9,A7,XTUPLE_0:1;
  end;
  suppose
A10: [i,p1] in the carrier' of S & [i,p2] in the carrier' of S;
    then consider j1 being (Element of NAT), q1 being FinSequence such that
A11: [i,p1] = [j1,q1] and
A12: len q1 = f.j1 and
    [:{j1}, (f.j1)-tuples_on underlay S:] c= the carrier' of S by A3;
A13: i = j1 & p1 = q1 by A11,XTUPLE_0:1;
    consider j2 being (Element of NAT), q2 being FinSequence such that
A14: [i,p2] = [j2,q2] and
A15: len q2 = f.j2 and
    [:{j2}, (f.j2)-tuples_on underlay S:] c= the carrier' of S by A3,A10;
    i = j2 by A14,XTUPLE_0:1;
    hence thesis by A12,A14,A15,A13,XTUPLE_0:1;
  end;
end;

theorem
  for S being delta-concrete ManySortedSign, i being set, p1,p2 being
  FinSequence st len p2 = len p1 & rng p2 c= underlay S holds ([i,p1] in the
carrier of S implies [i,p2] in the carrier of S) & ([i,p1] in the carrier' of S
  implies [i,p2] in the carrier' of S)
proof
  let S be delta-concrete ManySortedSign, i be set, p1,p2 be FinSequence such
  that
A1: len p2 = len p1 & rng p2 c= underlay S;
  consider f being Function of NAT,NAT such that
A2: for s being set st s in the carrier of S ex i being (Element of NAT)
  , p being FinSequence st s = [i,p] & len p = f.i & [:{i}, (f.i)-tuples_on
  underlay S:] c= the carrier of S and
A3: for o being set st o in the carrier' of S ex i being (Element of NAT
  ), p being FinSequence st o = [i,p] & len p = f.i & [:{i}, (f.i)-tuples_on
  underlay S:] c= the carrier' of S by Def7;
  hereby
    assume [i,p1] in the carrier of S;
    then consider j1 being (Element of NAT), q1 being FinSequence such that
A4: [i,p1] = [j1,q1] and
A5: len q1 = f.j1 and
A6: [:{j1}, (f.j1)-tuples_on underlay S:] c= the carrier of S by A2;
    p1 = q1 by A4,XTUPLE_0:1;
    then
A7: p2 in (f.j1)-tuples_on underlay S by A1,A5,FINSEQ_2:132;
    i = j1 by A4,XTUPLE_0:1;
    then [i,p2] in [:{j1}, (f.j1)-tuples_on underlay S:] by A7,ZFMISC_1:105;
    hence [i,p2] in the carrier of S by A6;
  end;
  assume [i,p1] in the carrier' of S;
  then consider j1 being (Element of NAT), q1 being FinSequence such that
A8: [i,p1] = [j1,q1] and
A9: len q1 = f.j1 and
A10: [:{j1}, (f.j1)-tuples_on underlay S:] c= the carrier' of S by A3;
  p1 = q1 by A8,XTUPLE_0:1;
  then
A11: p2 in (f.j1)-tuples_on underlay S by A1,A9,FINSEQ_2:132;
  i = j1 by A8,XTUPLE_0:1;
  then [i,p2] in [:{j1}, (f.j1)-tuples_on underlay S:] by A11,ZFMISC_1:105;
  hence thesis by A10;
end;

theorem
  for S being delta-concrete Categorial non empty Signature holds S is
  CatSignature of underlay S
proof
  let S be delta-concrete Categorial non empty Signature;
  set s = the SortSymbol of S;
  consider A being set such that
A1: CatSign A is Subsignature of S and
A2: the carrier of S = [:{0},2-tuples_on A:] by Def4;
  consider f being Function of NAT,NAT such that
A3: for s being set st s in the carrier of S ex i being (Element of NAT)
  , p being FinSequence st s = [i,p] & len p = f.i & [:{i}, (f.i)-tuples_on
  underlay S:] c= the carrier of S and
  for o being set st o in the carrier' of S ex i being (Element of NAT), p
being FinSequence st o = [i,p] & len p = f.i & [:{i}, (f.i)-tuples_on underlay
  S:] c= the carrier' of S by Def7;
  consider i being (Element of NAT), p being FinSequence such that
A4: s = [i,p] and
A5: len p = f.i & [:{i}, (f.i)-tuples_on underlay S:] c= the carrier of
  S by A3;
  p in 2-tuples_on A by A2,A4,ZFMISC_1:105;
  then
A6: len p = 2 by FINSEQ_2:132;
A7: A c= underlay S
  proof
    let x be set;
    assume x in A;
    then <*x,x*> in 2-tuples_on A by FINSEQ_2:137;
    then [0,<*x,x*>] in the carrier of S by A2,ZFMISC_1:105;
    then
A8: [0,<*x,x*>] in (the carrier of S) \/ the carrier' of S by XBOOLE_0:def 3;
    rng <*x,x*> = {x,x} by FINSEQ_2:127;
    then x in rng <*x,x*> by TARSKI:def 2;
    hence thesis by A8,Def6;
  end;
  i = 0 by A2,A4,ZFMISC_1:105;
  then
A9: 2-tuples_on underlay S c= 2-tuples_on A by A2,A5,A6,ZFMISC_1:94;
  underlay S c= A
  proof
    let x be set;
    assume x in underlay S;
    then <*x,x*> in 2-tuples_on underlay S by FINSEQ_2:137;
    hence thesis by A9,FINSEQ_2:138;
  end;
  then A = underlay S by A7,XBOOLE_0:def 10;
  hence thesis by A1,A2,Def5;
end;

begin :: Symbols of categorial sygnature

registration
  let S be non empty CatSignature;
  let s be SortSymbol of S;
  cluster s`2 -> Relation-like Function-like;
  coherence
  proof
    consider A being set such that
    CatSign A is Subsignature of S and
A1: the carrier of S = [:{0},2-tuples_on A:] by Def4;
    s`2 in 2-tuples_on A by A1,MCART_1:10;
    hence thesis;
  end;
end;

registration
  let S be non empty delta-concrete ManySortedSign;
  let s be SortSymbol of S;
  cluster s`2 -> Relation-like Function-like;
  coherence
  proof
    ex i being (Element of NAT), p being FinSequence st ( s = [ i,p])&( rng
    p c= underlay S) by Th6;
    hence thesis by MCART_1:7;
  end;
end;

registration
  let S be non void delta-concrete ManySortedSign;
  let o be Element of the carrier' of S;
  cluster o`2 -> Relation-like Function-like;
  coherence
  proof
    ex i being (Element of NAT), p being FinSequence st ( o = [ i,p])&( rng
    p c= underlay S) by Th6;
    hence thesis by MCART_1:7;
  end;
end;

registration
  let S be non empty CatSignature;
  let s be SortSymbol of S;
  cluster s`2 -> FinSequence-like;
  coherence
  proof
    consider A being set such that
    CatSign A is Subsignature of S and
A1: the carrier of S = [:{0},2-tuples_on A:] by Def4;
    s`2 in 2-tuples_on A by A1,MCART_1:10;
    then ex a,b being set st a in A & b in A & s`2 = <*a,b*> by FINSEQ_2:137;
    hence thesis;
  end;
end;

registration
  let S be non empty delta-concrete ManySortedSign;
  let s be SortSymbol of S;
  cluster s`2 -> FinSequence-like;
  coherence
  proof
    ex i being (Element of NAT), p being FinSequence st ( s = [ i,p])&( rng
    p c= underlay S) by Th6;
    hence thesis by MCART_1:7;
  end;
end;

registration
  let S be non void delta-concrete ManySortedSign;
  let o be Element of the carrier' of S;
  cluster o`2 -> FinSequence-like;
  coherence
  proof
    ex i being (Element of NAT), p being FinSequence st ( o = [ i,p])&( rng
    p c= underlay S) by Th6;
    hence thesis by MCART_1:7;
  end;
end;

definition
  let a be set;
  func idsym a equals
  [1,<*a*>];
  correctness;
  let b be set;
  func homsym(a,b) equals
  [0,<*a,b*>];
  correctness;
  let c be set;
  func compsym(a,b,c) equals
  [2,<*a,b,c*>];
  correctness;
end;

theorem Th10:
  for A being non empty set, S being CatSignature of A for a being
  Element of A holds idsym a in the carrier' of S & for b being Element of A
holds homsym(a,b) in the carrier of S & for c being Element of A holds compsym(
  a,b,c) in the carrier' of S
proof
  let A be non empty set, S be CatSignature of A;
  let a be Element of A;
A1: the carrier' of CatSign A = [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A
  :] by Def3;
A2: CatSign A is Subsignature of S by Def5;
  then
A3: the carrier of CatSign A c= the carrier of S by INSTALG1:10;
A4: the carrier' of CatSign A c= the carrier' of S by A2,INSTALG1:10;
  <*a*> in 1-tuples_on A by FINSEQ_2:135;
  then [1,<*a*>] in [:{1},1-tuples_on A:] by ZFMISC_1:105;
  then [1,<*a*>] in the carrier' of CatSign A by A1,XBOOLE_0:def 3;
  hence idsym a in the carrier' of S by A4;
  let b be Element of A;
A5: the carrier of CatSign A = [:{0},2-tuples_on A:] by Def3;
  <*a,b*> in 2-tuples_on A by FINSEQ_2:137;
  then [0,<*a,b*>] in [:{0},2-tuples_on A:] by ZFMISC_1:105;
  hence homsym(a,b) in the carrier of S by A3,A5;
  let c be Element of A;
  <*a,b,c*> in 3-tuples_on A by FINSEQ_2:139;
  then [2,<*a,b,c*>] in [:{2},3-tuples_on A:] by ZFMISC_1:105;
  then [2,<*a,b,c*>] in the carrier' of CatSign A by A1,XBOOLE_0:def 3;
  hence thesis by A4;
end;

definition
  let A be non empty set;
  let a be Element of A;
  redefine func idsym a -> OperSymbol of CatSign A;
  correctness by Th10;
  let b be Element of A;
  redefine func homsym(a,b) -> SortSymbol of CatSign A;
  correctness by Th10;
  let c be Element of A;
  redefine func compsym(a,b,c) -> OperSymbol of CatSign A;
  correctness by Th10;
end;

theorem Th11:
  for a,b being set st idsym(a) = idsym(b) holds a = b
proof
  let a,b be set;
  assume idsym(a) = idsym(b);
  then <*a*> = <*b*> by XTUPLE_0:1;
  hence thesis by Lm1;
end;

theorem Th12:
  for a1,b1,a2,b2 being set st homsym(a1,a2) = homsym(b1,b2) holds
  a1 = b1 & a2 = b2
proof
  let a1,b1,a2,b2 be set;
  assume homsym(a1,a2) = homsym(b1,b2);
  then
A1: <*a1,a2*> = <*b1,b2*> by XTUPLE_0:1;
  <*a1,a2*>.1 = a1 & <*a1,a2*>.2 = a2 by FINSEQ_1:44;
  hence thesis by A1,FINSEQ_1:44;
end;

theorem Th13:
  for a1,b1,a2,b2,a3,b3 being set st compsym(a1,a2,a3) = compsym(
  b1,b2,b3) holds a1 = b1 & a2 = b2 & a3 = b3
proof
  let a1,b1,a2,b2,a3,b3 be set;
A1: <*a1,a2,a3*>.3 = a3 by FINSEQ_1:45;
  assume compsym(a1,a2,a3) = compsym(b1,b2,b3);
  then
A2: <*a1,a2,a3*> = <*b1,b2,b3*> by XTUPLE_0:1;
  <*a1,a2,a3*>.1 = a1 & <*a1,a2,a3*>.2 = a2 by FINSEQ_1:45;
  hence thesis by A2,A1,FINSEQ_1:45;
end;

theorem Th14:
  for A being non empty set, S being CatSignature of A for s being
  SortSymbol of S ex a,b being Element of A st s = homsym(a,b)
proof
  let A be non empty set, S be CatSignature of A;
  let s be SortSymbol of S;
A1: the carrier of S = [:{0},2-tuples_on A:] by Def5;
  then s`2 in 2-tuples_on A by MCART_1:10;
  then s`2 in {z where z is Element of A*: len z = 2} by FINSEQ_2:def 4;
  then consider z being Element of A* such that
A2: s`2 = z and
A3: len z = 2;
A4: z.1 in {z.1,z.2} & z.2 in {z.1,z.2} by TARSKI:def 2;
A5: z = <*z.1,z.2*> by A3,FINSEQ_1:44;
  then rng z = {z.1,z.2} by FINSEQ_2:127;
  then reconsider a = z.1, b = z.2 as Element of A by A4;
  take a,b;
  s = [s`1,s`2] & s`1 in {0} by A1,MCART_1:10,21;
  hence thesis by A2,A5,TARSKI:def 1;
end;

theorem Th15:
  for A being non empty set, o being OperSymbol of CatSign A holds
  o`1 = 1 & len o`2 = 1 or o`1 = 2 & len o`2 = 3
proof
  let A be non empty set, o be OperSymbol of CatSign A;
  the carrier' of CatSign A = [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A
  :] by Def3;
  then o in [:{1},1-tuples_on A:] or o in [:{2},3-tuples_on A:] by
XBOOLE_0:def 3;
  then o`1 in {1} & o`2 in 1-tuples_on A or o`1 in {2} & o`2 in 3-tuples_on A
  by MCART_1:10;
  hence thesis by CARD_1:def 7,TARSKI:def 1;
end;

theorem Th16:
  for A being non empty set, o being OperSymbol of CatSign A st o
  `1 = 1 or len o`2 = 1 ex a being Element of A st o = idsym(a)
proof
  let A be non empty set, o be OperSymbol of CatSign A such that
A1: o`1 = 1 or len o`2 = 1;
  the carrier' of CatSign A = [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A
  :] by Def3;
  then o in [:{1},1-tuples_on A:] or o in [:{2},3-tuples_on A:] by
XBOOLE_0:def 3;
  then
A2: o`1 in {1} & o`2 in 1-tuples_on A & o = [o`1,o`2] or o`1 in {2} & o`2 in
  3-tuples_on A by MCART_1:10,21;
  then consider a being set such that
A3: a in A and
A4: o`2 = <*a*> by A1,CARD_1:def 7,FINSEQ_2:135,TARSKI:def 1;
  reconsider a as Element of A by A3;
  take a;
  thus thesis by A1,A2,A4,CARD_1:def 7,TARSKI:def 1;
end;

theorem Th17:
  for A being non empty set, o being OperSymbol of CatSign A st o
  `1 = 2 or len o`2 = 3 ex a,b,c being Element of A st o = compsym(a,b,c)
proof
  let A be non empty set, o be OperSymbol of CatSign A such that
A1: o`1 = 2 or len o`2 = 3;
  the carrier' of CatSign A = [:{1},1-tuples_on A:] \/ [:{2},3-tuples_on A
  :] by Def3;
  then o in [:{1},1-tuples_on A:] or o in [:{2},3-tuples_on A:] by
XBOOLE_0:def 3;
  then
A2: o`1 in {1} & o`2 in 1-tuples_on A or o`1 in {2} & o`2 in 3-tuples_on A &
  o = [o`1,o`2] by MCART_1:10,21;
  then consider a,b,c being set such that
A3: a in A & b in A & c in A and
A4: o`2 = <*a,b,c*> by A1,CARD_1:def 7,FINSEQ_2:139,TARSKI:def 1;
  reconsider a,b,c as Element of A by A3;
  take a,b,c;
  thus thesis by A1,A2,A4,CARD_1:def 7,TARSKI:def 1;
end;

theorem
  for A being non empty set, a being Element of A holds the_arity_of
  idsym(a) = {} & the_result_sort_of idsym(a) = homsym(a,a) by Def3;

theorem
  for A being non empty set, a,b,c being Element of A holds the_arity_of
compsym(a,b,c) = <*homsym(b,c),homsym(a,b)*> & the_result_sort_of compsym(a,b,c
  ) = homsym(a,c) by Def3;

begin :: Signature homomorphism generated by a functor

definition
  let C1,C2 be Category;
  let F be Functor of C1,C2;
  func Upsilon F -> Function of the carrier of CatSign the carrier of C1, the
  carrier of CatSign the carrier of C2 means
  : Def11:
  for s being SortSymbol of
  CatSign the carrier of C1 holds it.s = [0,(Obj F)*s`2];
  uniqueness
  proof
    let U1,U2 be Function of the carrier of CatSign the carrier of C1, the
    carrier of CatSign the carrier of C2 such that
A1: for s being SortSymbol of CatSign the carrier of C1 holds U1.s = [
    0,(Obj F)*s`2] and
A2: for s being SortSymbol of CatSign the carrier of C1 holds U2.s = [
    0,(Obj F)*s`2];
    now
      let s be SortSymbol of CatSign the carrier of C1;
      thus U1.s = [0,(Obj F)*s`2] by A1
        .= U2.s by A2;
    end;
    hence thesis by FUNCT_2:63;
  end;
  existence
  proof
    deffunc f(SortSymbol of CatSign the carrier of C1) = [0,(Obj F)*$1`2];
    consider Up being Function such that
A3: dom Up = the carrier of CatSign the carrier of C1 and
A4: for s being SortSymbol of CatSign the carrier of C1 holds Up.s = f
    (s) from FUNCT_1:sch 4;
    rng Up c= the carrier of CatSign the carrier of C2
    proof
      let x be set;
      assume x in rng Up;
      then consider a being set such that
A5:   a in dom Up and
A6:   x = Up.a by FUNCT_1:def 3;
      reconsider a as SortSymbol of CatSign the carrier of C1 by A3,A5;
      the carrier of CatSign the carrier of C1 = [:{0},2-tuples_on the
      carrier of C1:] by Def3;
      then a`2 in 2-tuples_on the carrier of C1 by MCART_1:12;
      then consider a1,a2 being set such that
A7:   a1 in the carrier of C1 & a2 in the carrier of C1 and
A8:   a`2 = <*a1,a2*> by FINSEQ_2:137;
      reconsider a1,a2 as Object of C1 by A7;
      rng <*a1,a2*> c= the carrier of C1 & dom Obj F = the carrier of C1
      by FUNCT_2:def 1;
      then
A9:   dom ((Obj F)*<*a1,a2*>) = dom <*a1,a2*> by RELAT_1:27
        .= Seg 2 by FINSEQ_1:89;
      then reconsider p = (Obj F)*<*a1,a2*> as FinSequence by FINSEQ_1:def 2;
      <*a1,a2*>.1 = a1 & 1 in {1,2} by FINSEQ_1:44,TARSKI:def 2;
      then
A10:  p.1 = (Obj F).a1 by A9,FINSEQ_1:2,FUNCT_1:12;
A11:  the carrier of CatSign the carrier of C2 = [:{0},2-tuples_on the
      carrier of C2:] by Def3;
      <*a1,a2*>.2 = a2 & 2 in {1,2} by FINSEQ_1:44,TARSKI:def 2;
      then
A12:  p.2 = (Obj F).a2 by A9,FINSEQ_1:2,FUNCT_1:12;
      len p = 2 by A9,FINSEQ_1:def 3;
      then p = <*(Obj F).a1, (Obj F).a2*> by A10,A12,FINSEQ_1:44;
      then p in 2-tuples_on the carrier of C2 by FINSEQ_2:101;
      then [0,p] in the carrier of CatSign the carrier of C2 by A11,
ZFMISC_1:105;
      hence thesis by A4,A6,A8;
    end;
    then Up is Function of the carrier of CatSign the carrier of C1, the
    carrier of CatSign the carrier of C2 by A3,FUNCT_2:def 1,RELSET_1:4;
    hence thesis by A4;
  end;
  func Psi F -> Function of the carrier' of CatSign the carrier of C1, the
  carrier' of CatSign the carrier of C2 means
  : Def12:
  for o being OperSymbol of
  CatSign the carrier of C1 holds it.o = [o`1,(Obj F)*o`2];
  uniqueness
  proof
    let U1,U2 be Function of the carrier' of CatSign the carrier of C1, the
    carrier' of CatSign the carrier of C2 such that
A13: for s being OperSymbol of CatSign the carrier of C1 holds U1.s =
    [s`1,(Obj F)*s`2] and
A14: for s being OperSymbol of CatSign the carrier of C1 holds U2.s =
    [s`1,(Obj F)*s`2];
    now
      let s be OperSymbol of CatSign the carrier of C1;
      thus U1.s = [s`1,(Obj F)*s`2] by A13
        .= U2.s by A14;
    end;
    hence thesis by FUNCT_2:63;
  end;
  existence
  proof
    deffunc f(OperSymbol of CatSign the carrier of C1) = [ $1`1,(Obj F)*$1`2 ];
    consider Up being Function such that
A15: dom Up = the carrier' of CatSign the carrier of C1 and
A16: for s being OperSymbol of CatSign the carrier of C1 holds Up.s =
    f(s) from FUNCT_1:sch 4;
    rng Up c= the carrier' of CatSign the carrier of C2
    proof
      let x be set;
      assume x in rng Up;
      then consider a being set such that
A17:  a in dom Up and
A18:  x = Up.a by FUNCT_1:def 3;
A19:  the carrier' of CatSign the carrier of C1 = [:{1},1-tuples_on the
      carrier of C1:] \/ [:{2},3-tuples_on the carrier of C1:] by Def3;
      reconsider a as OperSymbol of CatSign the carrier of C1 by A15,A17;
      per cases by A19,XBOOLE_0:def 3;
      suppose
A20:    a in [:{1},1-tuples_on the carrier of C1:];
        then a`2 in 1-tuples_on the carrier of C1 by MCART_1:12;
        then consider a1 being set such that
A21:    a1 in the carrier of C1 and
A22:    a`2 = <*a1*> by FINSEQ_2:135;
        reconsider a1 as Object of C1 by A21;
        rng <*a1*> c= the carrier of C1 & dom Obj F = the carrier of C1
        by FUNCT_2:def 1;
        then
A23:    dom ((Obj F)*<*a1*>) = dom <*a1*> by RELAT_1:27
          .= Seg 1 by FINSEQ_1:38;
        then reconsider p = (Obj F)*<*a1*> as FinSequence by FINSEQ_1:def 2;
A24:    len p = 1 by A23,FINSEQ_1:def 3;
        <*a1*>.1 = a1 & 1 in {1} by FINSEQ_1:40,TARSKI:def 1;
        then p.1 = (Obj F).a1 by A23,FINSEQ_1:2,FUNCT_1:12;
        then p = <*(Obj F).a1*> by A24,FINSEQ_1:40;
        then p is Element of 1-tuples_on the carrier of C2 by FINSEQ_2:98;
        then
A25:    [1,p] in [:{1},1-tuples_on the carrier of C2:] by ZFMISC_1:105;
A26:    a`1 = 1 by A20,MCART_1:12;
        the carrier' of CatSign the carrier of C2 = [:{1},1-tuples_on the
        carrier of C2:] \/ [:{2},3-tuples_on the carrier of C2:] by Def3;
        then [1,p] in the carrier' of CatSign the carrier of C2 by A25,
XBOOLE_0:def 3;
        hence thesis by A16,A18,A26,A22;
      end;
      suppose
A27:    a in [:{2},3-tuples_on the carrier of C1:];
        then a`2 in 3-tuples_on the carrier of C1 by MCART_1:12;
        then consider a1,a2,a3 being set such that
A28:    a1 in the carrier of C1 & a2 in the carrier of C1 & a3 in the
        carrier of C1 and
A29:    a`2 = <*a1,a2,a3*> by FINSEQ_2:139;
        reconsider a1,a2,a3 as Object of C1 by A28;
        rng <*a1,a2,a3*> c= the carrier of C1 & dom Obj F = the carrier
        of C1 by FUNCT_2:def 1;
        then
A30:    dom ((Obj F)*<*a1,a2,a3*>) = dom <*a1,a2,a3*> by RELAT_1:27
          .= Seg 3 by FINSEQ_1:89;
        then reconsider p = (Obj F)*<*a1,a2,a3*> as FinSequence by
FINSEQ_1:def 2;
        <*a1,a2,a3*>.1 = a1 & 1 in {1,2,3} by ENUMSET1:def 1,FINSEQ_1:45;
        then
A31:    p.1 = (Obj F).a1 by A30,FINSEQ_3:1,FUNCT_1:12;
        <*a1,a2,a3*>.3 = a3 & 3 in {1,2,3} by ENUMSET1:def 1,FINSEQ_1:45;
        then
A32:    p.3 = (Obj F). a3 by A30,FINSEQ_3:1,FUNCT_1:12;
        <*a1,a2,a3*>.2 = a2 & 2 in {1,2,3} by ENUMSET1:def 1,FINSEQ_1:45;
        then
A33:    p.2 = (Obj F).a2 by A30,FINSEQ_3:1,FUNCT_1:12;
        len p = 3 by A30,FINSEQ_1:def 3;
        then p = <*(Obj F).a1, (Obj F).a2, (Obj F).a3*> by A31,A33,A32,
FINSEQ_1:45;
        then p is Element of 3-tuples_on the carrier of C2 by FINSEQ_2:104;
        then
A34:    [2,p] in [:{2},3-tuples_on the carrier of C2:] by ZFMISC_1:105;
A35:    a`1 = 2 by A27,MCART_1:12;
        the carrier' of CatSign the carrier of C2 = [:{1},1-tuples_on the
        carrier of C2:] \/ [:{2},3-tuples_on the carrier of C2:] by Def3;
        then [2,p] in the carrier' of CatSign the carrier of C2 by A34,
XBOOLE_0:def 3;
        hence thesis by A16,A18,A35,A29;
      end;
    end;
    then Up is Function of the carrier' of CatSign the carrier of C1, the
    carrier' of CatSign the carrier of C2 by A15,FUNCT_2:def 1,RELSET_1:4;
    hence thesis by A16;
  end;
end;

Lm2: now
  let x be set, f be Function;
  assume x in dom f;
  then rng <*x*> = {x} & {x} c= dom f by FINSEQ_1:39,ZFMISC_1:31;
  then
A1: dom (f*<*x*>) = dom <*x*> by RELAT_1:27
    .= Seg 1 by FINSEQ_1:38;
  then reconsider p = f*<*x*> as FinSequence by FINSEQ_1:def 2;
A2: len p = 1 by A1,FINSEQ_1:def 3;
  1 in {1} & <*x*>.1 = x by FINSEQ_1:40,TARSKI:def 1;
  then p.1 = f.x by A1,FINSEQ_1:2,FUNCT_1:12;
  hence f*<*x*> = <*f.x*> by A2,FINSEQ_1:40;
end;

theorem Th20:
  for C1,C2 being Category, F being Functor of C1,C2 for a,b being
  Object of C1 holds (Upsilon F).homsym(a,b) = homsym(F.a,F.b)
proof
  let C1,C2 be Category, F be Functor of C1,C2;
  let a,b be Object of C1;
A1: dom Obj F = the carrier of C1 by FUNCT_2:def 1;
  thus (Upsilon F).homsym(a,b) = [0,(Obj F)*(homsym(a,b))`2] by Def11
    .= [0,(Obj F)*<*a,b*>] by MCART_1:7
    .= [0,<*(Obj F).a,(Obj F).b*>] by A1,FINSEQ_2:125
    .= [0,<*F.a,(Obj F).b*>]
    .= homsym(F.a,F.b);
end;

theorem Th21:
  for C1,C2 being Category, F being Functor of C1,C2 for a being
  Object of C1 holds (Psi F).idsym(a) = idsym(F.a)
proof
  let C1,C2 be Category, F be Functor of C1,C2;
  let a be Object of C1;
A1: dom Obj F = the carrier of C1 by FUNCT_2:def 1;
  (idsym a)`1 = 1 & (idsym a)`2 = <*a*> by MCART_1:7;
  hence (Psi F).idsym(a) = [1,(Obj F)*<*a*>] by Def12
    .= [1,<*(Obj F).a*>] by A1,Lm2
    .= idsym(F.a);
end;

theorem Th22:
  for C1,C2 being Category, F being Functor of C1,C2 for a,b,c
  being Object of C1 holds (Psi F).compsym(a,b,c) = compsym(F.a,F.b,F.c)
proof
  let C1,C2 be Category, F be Functor of C1,C2;
  let a,b,c be Object of C1;
A1: dom Obj F = the carrier of C1 by FUNCT_2:def 1;
  (compsym(a,b,c))`1 = 2 & (compsym(a,b,c))`2 = <*a,b,c*> by MCART_1:7;
  hence (Psi F).compsym(a,b,c) = [2,(Obj F)*<*a,b,c*>] by Def12
    .= [2,<*(Obj F).a,(Obj F).b,(Obj F).c*>] by A1,FINSEQ_2:126
    .= [2,<*F.a,(Obj F).b,(Obj F).c*>]
    .= [2,<*F.a,F.b,(Obj F).c*>]
    .= compsym(F.a,F.b,F.c);
end;

theorem Th23:
  for C1,C2 being Category, F being Functor of C1,C2 holds Upsilon
  F, Psi F form_morphism_between CatSign the carrier of C1, CatSign the carrier
  of C2
proof
  let C1,C2 be Category, F be Functor of C1,C2;
  set f = Upsilon F, g = Psi F;
  set S1 = CatSign the carrier of C1, S2 = CatSign the carrier of C2;
  thus dom f = the carrier of S1 & dom g = the carrier' of S1 by FUNCT_2:def 1;
  thus rng f c= the carrier of S2 & rng g c= the carrier' of S2;
  now
    let o be OperSymbol of CatSign the carrier of C1;
    per cases by Th15;
    suppose
      o`1 = 1;
      then consider a being Object of C1 such that
A1:   o = idsym(a) by Th16;
      thus (f*the ResultSort of S1).o = f.the_result_sort_of o by FUNCT_2:15
        .= f.homsym(a,a) by A1,Def3
        .= homsym(F.a,F.a) by Th20
        .= the_result_sort_of idsym(F.a) by Def3
        .= (the ResultSort of S2).(g.idsym a) by Th21
        .= ((the ResultSort of S2)*g).o by A1,FUNCT_2:15;
    end;
    suppose
      o`1 = 2;
      then consider a,b,c being Object of C1 such that
A2:   o = compsym(a,b,c) by Th17;
      thus (f*the ResultSort of S1).o = f.the_result_sort_of o by FUNCT_2:15
        .= f.homsym(a,c) by A2,Def3
        .= homsym(F.a,F.c) by Th20
        .= the_result_sort_of compsym(F.a,F.b,F.c) by Def3
        .= (the ResultSort of S2).(g.compsym(a,b,c)) by Th22
        .= ((the ResultSort of S2)*g).o by A2,FUNCT_2:15;
    end;
  end;
  hence f*the ResultSort of S1 = (the ResultSort of S2)*g by FUNCT_2:63;
  let o be set, p be Function;
  assume o in the carrier' of S1;
  then reconsider o9 = o as OperSymbol of S1;
  assume
A3: p = (the Arity of S1).o;
  per cases by Th15;
  suppose
    o9`1 = 1;
    then consider a being Object of C1 such that
A4: o = idsym(a) by Th16;
A5: f*{} = {};
    p = {} by A3,A4,Def3;
    hence f*p = the_arity_of idsym(F.a) by A5,Def3
      .= (the Arity of S2).(g.o) by A4,Th21;
  end;
  suppose
    o9`1 = 2;
    then consider a,b,c being Object of C1 such that
A6: o = compsym(a,b,c) by Th17;
    dom f = the carrier of S1 & p = <*homsym(b,c),homsym(a,b)*> by A3,A6,Def3,
FUNCT_2:def 1;
    hence f*p = <*f.homsym(b,c),f.homsym(a,b)*> by FINSEQ_2:125
      .= <*homsym(F.b,F.c),f.homsym(a,b)*> by Th20
      .= <*homsym(F.b,F.c),homsym(F.a,F.b)*> by Th20
      .= the_arity_of compsym(F.a,F.b,F.c) by Def3
      .= (the Arity of S2).(g.o) by A6,Th22;
  end;
end;

begin :: Algebra of morphisms

theorem Th24:
  for C being non empty set, A being MSAlgebra over CatSign C for
  a being Element of C holds Args(idsym(a), A) = {{}}
proof
  let C be non empty set, A be MSAlgebra over CatSign C;
  let a be Element of C;
  thus Args(idsym(a), A) = product ((the Sorts of A)*the_arity_of idsym a) by
PRALG_2:3
    .= product ((the Sorts of A)*{}) by Def3
    .= {{}} by CARD_3:10;
end;

Lm3: for C being Category, A being MSAlgebra over CatSign the carrier of C st
for a,b being Object of C holds (the Sorts of A).homsym(a,b) = Hom(a,b) for a,b
,c being Object of C holds Args(compsym(a,b,c), A) = product <*Hom(b,c),Hom(a,b
)*> & Result(compsym(a,b,c), A) = Hom(a,c)
proof
  let C be Category, A be MSAlgebra over CatSign the carrier of C;
  assume
A1: for a,b being Object of C holds (the Sorts of A).homsym(a,b) = Hom(a ,b);
  let a,b,c be Object of C;
A2: the carrier of CatSign the carrier of C = dom the Sorts of A by
PARTFUN1:def 2;
  thus Args(compsym(a,b,c), A) = product ((the Sorts of A)*the_arity_of
  compsym(a,b,c)) by PRALG_2:3
    .= product ((the Sorts of A)*<*homsym(b,c),homsym(a,b)*>) by Def3
    .= product <*(the Sorts of A).homsym(b,c), (the Sorts of A).homsym(a,b)
  *> by A2,FINSEQ_2:125
    .= product <*Hom(b,c), (the Sorts of A).homsym(a,b)*> by A1
    .= product <*Hom(b,c), Hom(a,b)*> by A1;
  thus Result(compsym(a,b,c), A) = (the Sorts of A).the_result_sort_of compsym
  (a,b,c) by PRALG_2:3
    .= (the Sorts of A).homsym(a,c) by Def3
    .= Hom(a,c) by A1;
end;

scheme
  CatAlgEx { X, Y() -> non empty set, H(set,set) -> set, R(set,set,set,set,set
) -> set, I(set) -> set}: ex A being strict MSAlgebra over CatSign X() st (for
a,b being Element of X() holds (the Sorts of A).homsym(a,b) = H(a,b)) & (for a
being Element of X() holds Den(idsym(a),A).{} = I(a)) & for a,b,c being Element
  of X() for f,g being Element of Y() st f in H(a,b) & g in H(b,c) holds Den(
  compsym(a,b,c),A).<*g,f*> = R(a,b,c,g,f)
provided
A1: for a,b being Element of X() holds H(a,b) c= Y() and
A2: for a being Element of X() holds I(a) in H(a,a) and
A3: for a,b,c being Element of X() for f,g being Element of Y() st f in
H(a,b) & g in H(b,c) holds R(a,b,c,g,f) in H(a,c)
proof
  defpred Z[set,set] means ($1`1 = 1 & ex a being Element of X() st $1 = idsym
(a) & ex F being Function of {{}}, H(a,a) st F = $2 & F.{} = I(a)) or ($1`1 = 2
& ex a,b,c being Element of X() st $1 = compsym(a,b,c) & ex F being Function of
product<*H(b,c),H(a,b)*>, H(a,c) st F = $2 & for f,g being set st f in H(a,b) &
  g in H(b,c) holds F.<*g,f*> = R(a,b,c,g,f));
  set CS = CatSign X();
A4: for o be set st o in the carrier' of CS ex u be set st Z[o,u]
  proof
    let o be set;
    assume
A5: o in the carrier' of CS;
A6: now
      assume o`1 = 1;
      then consider a being Element of X() such that
A7:   o = idsym a by A5,Th16;
      set F = {} :-> I(a);
      reconsider u = F as set;
      take u, a;
      thus o = idsym(a) by A7;
      I(a) in H(a,a) by A2;
      then {I(a)} c= H(a,a) by ZFMISC_1:31;
      then dom F = {{}} & rng F c= H(a,a) by FUNCOP_1:13,XBOOLE_1:1;
      then reconsider F as Function of {{}}, H(a,a) by FUNCT_2:2;
      take F;
      {} in {{}} by TARSKI:def 1;
      hence F = u & F.{} = I(a) by FUNCOP_1:7;
    end;
A8: now
      assume o`1 = 2;
      then consider a,b,c being Element of X() such that
A9:   o = compsym(a,b,c) by A5,Th17;
      defpred P[set,set] means ex f,g being set st f in H(a,b) & g in H(b,c) &
      $1 = <*g,f*> & $2 = R(a,b,c,g,f);
A10:  now
        let x be set;
        assume x in product<*H(b,c),H(a,b)*>;
        then consider g,f being set such that
A11:    g in H(b,c) & f in H(a,b) and
A12:    x = <*g,f*> by FINSEQ_3:124;
        take u = R(a,b,c,g,f);
        H(a,b) c= Y() & H(b,c) c= Y() by A1;
        hence u in H(a,c) by A3,A11;
        thus P[x,u] by A11,A12;
      end;
      consider F being Function such that
A13:  dom F = product<*H(b,c),H(a,b)*> & rng F c= H(a,c) and
A14:  for x being set st x in product<*H(b,c),H(a,b)*> holds P[x,F.x]
      from FUNCT_1:sch 5(A10);
      reconsider u = F as set;
      take u, a, b, c;
      thus o = compsym(a,b,c) by A9;
      reconsider F as Function of product<*H(b,c),H(a,b)*>, H(a,c) by A13,
FUNCT_2:2;
      take F;
      thus F = u;
      let f,g be set;
      assume f in H(a,b) & g in H(b,c);
      then <*g,f*> in product<*H(b,c),H(a,b)*> by FINSEQ_3:124;
      then consider f9,g9 being set such that
      f9 in H(a,b) and
      g9 in H(b,c) and
A15:  <*g,f*> = <*g9,f9*> and
A16:  F.<*g,f*> = R(a,b,c,g9,f9) by A14;
A17:  <*g,f*>.1 = g & <*g,f*>.2 = f by FINSEQ_1:44;
      <*g,f*>.1 = g9 by A15,FINSEQ_1:44;
      hence F.<*g,f*> = R(a,b,c,g,f) by A15,A16,A17,FINSEQ_1:44;
    end;
    o`1 = 1 or o`1 = 2 by A5,Th15;
    hence thesis by A6,A8;
  end;
  consider O being Function such that
A18: dom O = the carrier' of CS and
A19: for o being set st o in the carrier' of CS holds Z[o,O.o] from
  CLASSES1:sch 1(A4);
  reconsider O as ManySortedSet of the carrier' of CS by A18,PARTFUN1:def 2
,RELAT_1:def 18;
  defpred P[set,set] means ex a,b being Element of X() st $1 = homsym(a,b) &
  $2 = H(a,b);
A20: now
    let s be set;
    assume s in the carrier of CS;
    then consider a,b being Element of X() such that
A21: s = homsym(a,b) by Th14;
    take u = H(a,b);
    thus P[s,u] by A21;
  end;
  consider S being Function such that
A22: dom S = the carrier of CS and
A23: for s being set st s in the carrier of CS holds P[s,S.s] from
  CLASSES1:sch 1(A20);
  reconsider S as ManySortedSet of the carrier of CS by A22,PARTFUN1:def 2
,RELAT_1:def 18;
  O is ManySortedFunction of S#*the Arity of CS, S*the ResultSort of CS
  proof
    let o be set;
    assume o in the carrier' of CS;
    then reconsider o as OperSymbol of CS;
A24: (S#*the Arity of CS).o = S#.the_arity_of o by FUNCT_2:15
      .= product (S*the_arity_of o) by FINSEQ_2:def 5;
A25: (S*the ResultSort of CS).o = S.the_result_sort_of o by FUNCT_2:15;
    per cases by Th15;
    suppose
      o`1 = 1 & 1 <> 2;
      then consider a being Element of X() such that
A26:  o = idsym a & ex F being Function of {{}}, H(a,a) st F = O.o &
      F.{} = I(a) by A19;
A27:  the_arity_of idsym(a) = {} & {} = S*{} by Def3;
A28:  the_result_sort_of idsym(a) = homsym(a,a) by Def3;
      consider c,b being Element of X() such that
A29:  homsym(a,a) = homsym(c,b) and
A30:  S.homsym(a,a) = H(c,b) by A23;
      a = b & a = c by A29,Th12;
      hence thesis by A24,A25,A26,A30,A27,A28,CARD_3:10;
    end;
    suppose
      o`1 = 2 & 1 <> 2;
      then consider a,b,c being Element of X() such that
A31:  o = compsym(a,b,c) and
A32:  ex F being Function of product<*H(b,c),H(a,b)*>, H(a,c) st F =
O.o & for f,g being set st f in H(a,b) & g in H(b,c) holds F.<*g,f*> = R(a,b,c,
      g,f) by A19;
A33:  the_result_sort_of compsym(a,b,c) = homsym(a,c) by Def3;
      consider ax,cx being Element of X() such that
A34:  homsym(a,c) = homsym(ax,cx) and
A35:  S.homsym(a,c) = H(ax,cx) by A23;
      ax = a & cx = c by A34,Th12;
      then
A36:  (S*the ResultSort of CS).o = H(a,c) by A31,A35,A33,FUNCT_2:15;
A37:  the_arity_of compsym(a,b,c) = <*homsym(b,c),homsym(a,b)*> by Def3;
      consider a9,b9 being Element of X() such that
A38:  homsym(a,b) = homsym(a9,b9) and
A39:  S.homsym(a,b) = H(a9,b9) by A23;
      consider b99,c9 being Element of X() such that
A40:  homsym(b,c) = homsym(b99,c9) and
A41:  S.homsym(b,c) = H(b99,c9) by A23;
A42:  b99 = b & c9 = c by A40,Th12;
      a9 = a & b9 = b by A38,Th12;
      then
      (S#*the Arity of CS).o = product<*H(b,c),H(a,b)*> by A22,A24,A31,A39,A41
,A42,A37,FINSEQ_2:125;
      hence thesis by A32,A36;
    end;
  end;
  then reconsider
  O as ManySortedFunction of S#*the Arity of CS, S*the ResultSort
  of CS;
  take A = MSAlgebra(#S, O#);
  hereby
    let a,b be Element of X();
    consider a9,b9 being Element of X() such that
A43: homsym(a,b) = homsym(a9,b9) and
A44: S.homsym(a,b) = H(a9,b9) by A23;
    a = a9 by A43,Th12;
    hence (the Sorts of A).homsym(a,b) = H(a,b) by A43,A44,Th12;
  end;
  hereby
    let a be Element of X();
    (idsym a)`1 = 1 by MCART_1:7;
    then ex b being Element of X() st idsym a = idsym b & ex F being Function
    of {{}}, H(b,b) st F = O.idsym a & F.{} = I(b) by A19;
    hence Den(idsym(a),A).{} = I(a) by Th11;
  end;
  let a,b,c be Element of X();
  set o = compsym(a,b,c);
  o`1 = 2 by MCART_1:7;
  then consider a9,b9,c9 being Element of X() such that
A45: o = compsym(a9,b9,c9) and
A46: ex F being Function of product<*H(b9,c9),H(a9,b9)*>, H(a9,c9) st F
= O.o & for f,g being set st f in H(a9,b9) & g in H(b9,c9) holds F.<*g,f*> = R(
  a9,b9,c9,g,f) by A19;
A47: c = c9 by A45,Th13;
  let f,g be Element of Y();
  assume
A48: f in H(a,b) & g in H(b,c);
  a = a9 & b = b9 by A45,Th13;
  hence thesis by A46,A47,A48;
end;

definition
  let C be Category;
  func MSAlg C -> strict MSAlgebra over CatSign the carrier of C means
  : Def13
  :
  ( for a,b being Object of C holds (the Sorts of it).homsym(a,b) = Hom(a,b)) &
  (for a being Object of C holds Den(idsym(a),it).{} = id a) & for a,b,c being
Object of C for f,g being Morphism of C st dom f = a & cod f = b & dom g = b &
  cod g = c holds Den(compsym(a,b,c),it).<*g,f*> = g(*)f;
  uniqueness
  proof
    let A1,A2 be strict MSAlgebra over CatSign the carrier of C such that
A1: for a,b being Object of C holds (the Sorts of A1).homsym(a,b) =
    Hom(a,b) and
A2: for a being Object of C holds Den(idsym(a),A1).{} = id a and
A3: for a,b,c being Object of C for f,g being Morphism of C st dom f =
a & cod f = b & dom g = b & cod g = c
  holds Den(compsym(a,b,c),A1).<*g,f*> = g(*)
    f and
A4: for a,b being Object of C holds (the Sorts of A2).homsym(a,b) =
    Hom(a,b) and
A5: for a being Object of C holds Den(idsym(a),A2).{} = id a and
A6: for a,b,c being Object of C for f,g being Morphism of C st dom f =
a & cod f = b & dom g = b & cod g = c
   holds Den(compsym(a,b,c),A2).<*g,f*> = g(*)
    f;
A7: now
      let i be set;
      assume i in the carrier' of CatSign the carrier of C;
      then reconsider o = i as OperSymbol of CatSign the carrier of C;
      per cases by Th15;
      suppose
        o`1 = 1;
        then consider a being Object of C such that
A8:     o = idsym(a) by Th16;
A9:     id a in Hom(a,a) by CAT_1:27;
A10:    the_result_sort_of idsym a = homsym(a,a) by Def3;
        (the Sorts of A1).homsym(a,a) = Hom(a,a) by A1;
        then Result(idsym a,A1) = Hom(a,a) by A10,PRALG_2:3;
        then
A11:    dom Den(idsym a,A1) = Args(idsym a,A1) by A9,FUNCT_2:def 1;
A12:    now
          let x be set;
          assume x in {{}};
          then
A13:      x = {} by TARSKI:def 1;
          then Den(idsym a,A1).x = id a by A2;
          hence Den(idsym a,A1).x = Den(idsym a,A2).x by A5,A13;
        end;
        (the Sorts of A2).homsym(a,a) = Hom(a,a) by A4;
        then Result(idsym a,A2) = Hom(a,a) by A10,PRALG_2:3;
        then
A14:    dom Den(idsym a,A2) = Args(idsym a,A2) by A9,FUNCT_2:def 1;
        Args(idsym a,A1) = {{}} & Args(idsym a,A2) = {{}} by Th24;
        hence (the Charact of A1).i = (the Charact of A2).i by A8,A11,A14,A12,
FUNCT_1:2;
      end;
      suppose
        o`1 = 2;
        then consider a,b,c being Object of C such that
A15:    o = compsym(a,b,c) by Th17;
A16:    now
          assume product <*Hom(b,c),Hom(a,b)*> <> {};
          then reconsider X = product <*Hom(b,c),Hom(a,b)*> as non empty set;
          set x = the Element of X;
          consider g,f being set such that
A17:      g in Hom(b,c) and
A18:      f in Hom(a,b) and
          x = <*g,f*> by FINSEQ_3:124;
          reconsider g,f as Morphism of C by A17,A18;
A19:      cod f = b & dom g = b by A17,A18,CAT_1:1;
          cod g = c by A17,CAT_1:1;
          then
A20:      cod (g(*)f) = c by A19,CAT_1:17;
          dom f = a by A18,CAT_1:1;
          then dom (g(*)f) = a by A19,CAT_1:17;
          hence Hom(a,c) <> {} by A20,CAT_1:1;
        end;
A21:    now
          let x be set;
          assume x in product <*Hom(b,c),Hom(a,b)*>;
          then consider g,f being set such that
A22:      g in Hom(b,c) and
A23:      f in Hom(a,b) and
A24:      x = <*g,f*> by FINSEQ_3:124;
          reconsider g,f as Morphism of C by A22,A23;
A25:      dom g = b & cod g = c by A22,CAT_1:1;
A26:      dom f = a & cod f = b by A23,CAT_1:1;
          then Den(compsym(a,b,c),A1).x = g(*)f by A3,A24,A25;
          hence Den(compsym(a,b,c),A1).x = Den(compsym(a,b,c),A2).x by A6,A24
,A26,A25;
        end;
A27:    Args(compsym(a,b,c),A1) = product <*Hom(b,c),Hom(a,b)*> by A1,Lm3;
A28:    Args(compsym(a,b,c),A2) = product <*Hom(b,c),Hom(a,b)*> by A4,Lm3;
        Result(compsym(a,b,c),A2) = Hom(a,c) by A4,Lm3;
        then
A29:    dom Den(compsym(a,b,c),A2) = Args(compsym(a,b,c),A2) by A28,A16,
FUNCT_2:def 1;
        Result(compsym(a,b,c),A1) = Hom(a,c) by A1,Lm3;
        then dom Den(compsym(a,b,c),A1) = Args(compsym(a,b,c),A1) by A27,A16,
FUNCT_2:def 1;
        hence (the Charact of A1).i = (the Charact of A2).i by A15,A27,A28,A29
,A21,FUNCT_1:2;
      end;
    end;
    now
      let i be set;
      assume i in the carrier of CatSign the carrier of C;
      then consider a,b being Object of C such that
A30:  i = homsym(a,b) by Th14;
      thus (the Sorts of A1).i = Hom(a,b) by A1,A30
        .= (the Sorts of A2).i by A4,A30;
    end;
    then the Sorts of A1 = the Sorts of A2 by PBOOLE:3;
    hence thesis by A7,PBOOLE:3;
  end;
  correctness
  proof
    deffunc I(Object of C) = id $1;
    deffunc R(Object of C,Object of C,Object of C, (Morphism of C), Morphism
    of C) = $4(*)$5;
    deffunc H(Object of C,Object of C) = Hom($1,$2);
A31: for a being Object of C holds I(a) in H(a,a) by CAT_1:27;
A32: now
      let a,b,c be Object of C, f,g be Morphism of C;
      assume that
A33:  f in H(a,b) and
A34:  g in H(b,c);
A35:  cod f = b & dom g = b by A33,A34,CAT_1:1;
      cod g = c by A34,CAT_1:1;
      then
A36:  cod (g(*)f) = c by A35,CAT_1:17;
      dom f = a by A33,CAT_1:1;
      then dom (g(*)f) = a by A35,CAT_1:17;
      hence R(a,b,c,g,f) in H(a,c) by A36;
    end;
A37: for a,b being Object of C holds H(a,b) c= the carrier' of C;
    consider A being strict MSAlgebra over CatSign the carrier of C such that
A38: ( for a,b being Element of C holds (the Sorts of A
    ).homsym(a,b) = H(a,b))& for a being Element of C holds Den(
    idsym(a),A).{} = I(a) and
A39: for a,b,c being Element of C for f,g being Element
of the carrier' of C st f in H(a,b) & g in H(b,c) holds Den(compsym(a,b,c),A).
    <*g,f*> = R(a,b,c,g,f) from CatAlgEx(A37,A31,A32);
    take A;
    now
      let a,b,c be Object of C, f,g be Morphism of C;
      assume dom f = a & cod f = b & dom g = b & cod g = c;
      then f in Hom(a,b) & g in Hom(b,c);
      hence Den(compsym(a,b,c),A).<*g,f*> = g(*)f by A39;
    end;
    hence thesis by A38;
  end;
end;

theorem Th25:
  for A being Category, a being Object of A holds Result(idsym a,
  MSAlg A) = Hom(a,a)
proof
  let A be Category, a be Object of A;
  thus Result(idsym a, MSAlg A) = (the Sorts of MSAlg A).the_result_sort_of
  idsym a by PRALG_2:3
    .= (the Sorts of MSAlg A).homsym(a,a) by Def3
    .= Hom(a,a) by Def13;
end;

theorem Th26:
  for A being Category, a,b,c being Object of A holds Args(compsym
  (a,b,c), MSAlg A) = product <*Hom(b,c), Hom(a,b)*> & Result(compsym(a,b,c),
  MSAlg A) = Hom(a,c)
proof
  let A be Category, a,b,c be Object of A;
  for a,b being Object of A holds (the Sorts of MSAlg A).homsym(a,b) = Hom
  (a,b) by Def13;
  hence thesis by Lm3;
end;

registration
  let C be Category;
  cluster MSAlg C -> disjoint_valued feasible;
  coherence
  proof
    hereby
      let x,y be set;
      assume that
A1:   x <> y and
A2:   (the Sorts of MSAlg C).x meets (the Sorts of MSAlg C).y;
      consider z being set such that
A3:   z in (the Sorts of MSAlg C).x and
A4:   z in (the Sorts of MSAlg C).y by A2,XBOOLE_0:3;
      dom the Sorts of MSAlg C = the carrier of CatSign the carrier of C
      by PARTFUN1:def 2;
      then reconsider x,y as SortSymbol of CatSign the carrier of C by A3,A4,
FUNCT_1:def 2;
      consider a,b being Object of C such that
A5:   x = homsym(a,b) by Th14;
A6:   z in Hom(a,b) by A3,A5,Def13;
      consider c,d being Object of C such that
A7:   y = homsym(c,d) by Th14;
A8:   z in Hom(c,d) by A4,A7,Def13;
      reconsider z as Morphism of C by A6;
A9:   dom z = a & cod z = b by A6,CAT_1:1;
      dom z = c by A8,CAT_1:1;
      hence contradiction by A1,A5,A7,A8,A9,CAT_1:1;
    end;
    let o be OperSymbol of CatSign the carrier of C;
    per cases by Th15;
    suppose
      o`1 = 1;
      then consider a being Object of C such that
A10:  o = idsym a by Th16;
      Result(o, MSAlg C) = Hom(a,a) by A10,Th25;
      hence thesis by CAT_1:27;
    end;
    suppose
      o`1 = 2;
      then consider a,b,c being Object of C such that
A11:  o = compsym(a,b,c) by Th17;
      set A = the Element of Args(o, MSAlg C);
      assume
A12:  Args(o, MSAlg C) <> {};
      Args(o, MSAlg C) = product <*Hom(b,c), Hom(a,b)*> by A11,Th26;
      then
A13:  ex g,f being set st g in Hom(b,c) & f in Hom(a,b) & A = <*g,f*> by A12,
FINSEQ_3:124;
      Result(o, MSAlg C) = Hom(a,c) by A11,Th26;
      hence thesis by A13,CAT_1:24;
    end;
  end;
end;

theorem Th27:
  for C1,C2 being Category, F being Functor of C1,C2 holds F-MSF(
  the carrier of CatSign the carrier of C1, the Sorts of MSAlg C1) is
ManySortedFunction of MSAlg C1, (MSAlg C2)|(CatSign the carrier of C1, Upsilon
  F, Psi F)
proof
  let C1,C2 be Category, F be Functor of C1,C2;
  set S1 = CatSign the carrier of C1, S2 = CatSign the carrier of C2;
  set A1 = MSAlg C1, A2 = MSAlg C2;
  set f = Upsilon F, g = Psi F, B1 = A2|(S1, f, g);
  set H = F-MSF(the carrier of S1, the Sorts of A1);
  let i be set;
  assume i in the carrier of S1;
  then reconsider s = i as SortSymbol of S1;
  consider a,b being Object of C1 such that
A1: s = homsym(a,b) by Th14;
  f, g form_morphism_between S1,S2 by Th23;
  then the Sorts of B1 = (the Sorts of A2)*f by INSTALG1:def 3;
  then
A2: (the Sorts of A2).(f.s) = (the Sorts of B1).s by FUNCT_2:15;
  f.s = homsym(F.a,F.b) by A1,Th20;
  then
A3: (the Sorts of A2).(f.s) = Hom(F.a,F.b) by Def13;
A4: (the Sorts of A1).s = Hom(a,b) by A1,Def13;
  H.s = F|((the Sorts of A1).s) by Def1;
  then H.s = hom(F,a,b) by A4;
  hence thesis by A2,A4,A3;
end;

theorem Th28:
  for C being Category, a,b,c being Object of C for x being set
holds x in Args(compsym(a,b,c), MSAlg C) iff ex g,f being Morphism of C st x =
  <*g,f*> & dom f = a & cod f = b & dom g = b & cod g = c
proof
  let C be Category, a,b,c be Object of C, x be set;
  set A = MSAlg C;
  for a,b being Object of C holds (the Sorts of A).homsym(a,b) = Hom(a,b )
  by Def13;
  then
A1: Args(compsym(a,b,c), A) = product <*Hom(b,c),Hom(a,b)*> by Lm3;
  hereby
    assume x in Args(compsym(a,b,c), A);
    then consider g,f being set such that
A2: g in Hom(b,c) & f in Hom(a,b) and
A3: x = <*g,f*> by A1,FINSEQ_3:124;
    reconsider g,f as Morphism of C by A2;
    take g,f;
    thus x = <*g,f*> by A3;
    thus dom f = a & cod f = b & dom g = b & cod g = c by A2,CAT_1:1;
  end;
  given g,f being Morphism of C such that
A4: x = <*g,f*> and
A5: dom f = a & cod f = b & dom g = b & cod g = c;
  f in Hom(a,b) & g in Hom(b,c) by A5;
  hence thesis by A1,A4,FINSEQ_3:124;
end;

theorem Th29:
  for C1,C2 being Category, F being Functor of C1,C2 for a,b,c
being Object of C1 for f,g being Morphism of C1 st f in Hom(a,b) & g in Hom(b,c
  ) for x being Element of Args(compsym(a,b,c),MSAlg C1) st x = <*g,f*> for H
  being ManySortedFunction of MSAlg C1, (MSAlg C2)|(CatSign the carrier of C1,
  Upsilon F, Psi F) st H = F-MSF(the carrier of CatSign the carrier of C1, the
  Sorts of MSAlg C1) holds H#x = <*F.g,F.f*>
proof
  let C1,C2 be Category, F be Functor of C1,C2;
  set CS1 = CatSign the carrier of C1, CS2 = CatSign the carrier of C2;
  set A1 = MSAlg C1, A2 = MSAlg C2;
  set u = Upsilon F, p = Psi F;
  set B = A2|(CS1, u, p);
  let a,b,c be Object of C1;
  set o = compsym(a,b,c);
  let f,g be Morphism of C1 such that
A1: f in Hom(a,b) and
A2: g in Hom(b,c);
  let x be Element of Args(o, A1) such that
A3: x = <*g,f*>;
  F.g in Hom(F.b,F.c) by A2,CAT_1:81;
  then
A4: dom (F.g) = F.b & cod (F.g) = F.c by CAT_1:1;
  F.f in Hom(F.a,F.b) by A1,CAT_1:81;
  then dom (F.f) = F.a & cod (F.f) = F.b by CAT_1:1;
  then
A5: <*F.g,F.f*> in Args(compsym(F.a,F.b,F.c), A2) by A4,Th28;
A6: dom g = b & cod g = c by A2,CAT_1:1;
  dom f = a & cod f = b by A1,CAT_1:1;
  then
A7: x in Args(o, A1) by A3,A6,Th28;
  let H be ManySortedFunction of A1, B such that
A8: H = F-MSF(the carrier of CS1, the Sorts of A1);
  (the Sorts of A1).homsym(b,c) = Hom(b,c) by Def13;
  then H.homsym(b,c) = F|Hom(b,c) by A8,Def1;
  then
A9: (H.homsym(b,c)).g = F.g by A2,FUNCT_1:49;
A10: dom <*g,f*> = Seg 2 by FINSEQ_1:89;
  then
A11: 1 in dom <*g,f*> by FINSEQ_1:2,TARSKI:def 2;
  (the Sorts of A1).homsym(a,b) = Hom(a,b) by Def13;
  then H.homsym(a,b) = F|Hom(a,b) by A8,Def1;
  then
A12: (H.homsym(a,b)).f = F.f by A1,FUNCT_1:49;
A13: 2 in dom <*g,f*> by A10,FINSEQ_1:2,TARSKI:def 2;
  u,p form_morphism_between CS1, CS2 by Th23;
  then
A14: Args(o, B) = Args(p.o, A2) by INSTALG1:24
    .= Args(compsym(F.a,F.b,F.c), A2) by Th22;
  then consider g9,f9 being Morphism of C2 such that
A15: H#x = <*g9,f9*> and
  dom f9 = F.a and
  cod f9 = F.b and
  dom g9 = F.b and
  cod g9 = F. c by A5,Th28;
A16: <*g9,f9*>.1 = g9 by FINSEQ_1:44;
A17: the_arity_of o = <*homsym(b,c),homsym(a,b)*> by Def3;
  then <*g,f*>.1 = g & (the_arity_of o)/.1 = homsym(b,c) by FINSEQ_1:44
,FINSEQ_4:17;
  then
A18: <*g9,f9*>.1 = F.g by A3,A7,A5,A14,A15,A9,A11,MSUALG_3:24;
  <*g,f*>.2 = f & (the_arity_of o)/.2 = homsym(a,b ) by A17,FINSEQ_1:44
,FINSEQ_4:17;
  then <*g9,f9*>.2 = F.f by A3,A7,A5,A14,A15,A12,A13,MSUALG_3:24;
  hence thesis by A15,A18,A16,FINSEQ_1:44;
end;

theorem Th30:
  for C being Category, a,b,c being Object of C, f,g being
Morphism of C st f in Hom(a,b) & g in Hom(b,c) holds Den(compsym(a,b,c), MSAlg
  C).<*g,f*> = g(*)f
proof
  let C be Category, a,b,c be Object of C, f,g be Morphism of C;
  assume that
A1: f in Hom(a,b) and
A2: g in Hom(b,c);
A3: dom g = b & cod g = c by A2,CAT_1:1;
  dom f = a & cod f = b by A1,CAT_1:1;
  hence thesis by A3,Def13;
end;

theorem
  for C being Category, a,b,c,d being Object of C, f,g,h being Morphism
of C st f in Hom(a,b) & g in Hom(b,c) & h in Hom(c,d) holds Den(compsym(a,c,d),
  MSAlg C).<*h, Den(compsym(a,b,c), MSAlg C).<*g,f*>*> = Den(compsym(a,b,d),
  MSAlg C).<*Den(compsym(b,c,d), MSAlg C).<*h,g*>, f*>
proof
  let C be Category, a,b,c,d be Object of C, f,g,h be Morphism of C;
  assume that
A1: f in Hom(a,b) and
A2: g in Hom(b,c) and
A3: h in Hom(c,d);
A4: cod g = c by A2,CAT_1:1;
A5: Den(compsym(b,c,d), MSAlg C).<*h,g*> = h(*)g by A2,A3,Th30;
A6: cod f = b by A1,CAT_1:1;
A7: dom h = c by A3,CAT_1:1;
  cod h = d by A3,CAT_1:1;
  then
A8: cod (h(*)g) = d by A4,A7,CAT_1:17;
A9: dom g = b by A2,CAT_1:1;
  then dom (h(*)g) = b by A4,A7,CAT_1:17;
  then
A10: h(*)g in Hom(b,d) by A8;
  dom f = a by A1,CAT_1:1;
  then
A11: dom (g(*)f) = a by A6,A9,CAT_1:17;
  cod (g(*)f) = c by A6,A9,A4,CAT_1:17;
  then
A12: g(*)f in Hom(a,c) by A11;
  Den(compsym(a,b,c), MSAlg C).<*g,f*> = g(*)f by A1,A2,Th30;
  hence Den(compsym(a,c,d), MSAlg C).<*h, Den(compsym(a,b,c), MSAlg C).<*g,f*>
  *> = h(*)(g(*)f) by A3,A12,Th30
    .= (h(*)g)(*)f by A6,A9,A4,A7,CAT_1:18
    .= Den(compsym(a,b,d),MSAlg C).<*Den(compsym(b,c,d),MSAlg C).<*h,g*>,f*>
  by A1,A5,A10,Th30;
end;

theorem
  for C being Category, a,b being Object of C, f being Morphism of C st
f in Hom(a,b) holds Den(compsym(a,b,b), MSAlg C).<*id b, f*> = f & Den(compsym(
  a,a,b), MSAlg C).<*f, id a*> = f
proof
  let C be Category, a,b be Object of C, f be Morphism of C;
  assume
A1: f in Hom(a,b);
  then dom f = a by CAT_1:1;
  then
A2: f(*)id a = f by CAT_1:22;
  cod f = b by A1,CAT_1:1;
  then
A3: (id b)(*)f = f by CAT_1:21;
  id b in Hom(b,b) & id a in Hom(a,a) by CAT_1:27;
  hence thesis by A1,A3,A2,Th30;
end;

theorem
  for C1,C2 being Category, F being Functor of C1,C2 ex H being
ManySortedFunction of MSAlg C1, (MSAlg C2)|(CatSign the carrier of C1, Upsilon
  F, Psi F) st H = F-MSF(the carrier of CatSign the carrier of C1, the Sorts of
MSAlg C1) & H is_homomorphism MSAlg C1, (MSAlg C2)|(CatSign the carrier of C1,
  Upsilon F, Psi F)
proof
  let C1,C2 be Category, F be Functor of C1,C2;
  set S1 = CatSign the carrier of C1, S2 = CatSign the carrier of C2;
  set A1 = MSAlg C1, A2 = MSAlg C2;
  set f = Upsilon F, G = Psi F;
  set B1 = A2|(S1, f, G);
A1: f, G form_morphism_between S1,S2 by Th23;
  reconsider H = F-MSF(the carrier of S1, the Sorts of A1) as
  ManySortedFunction of A1,B1 by Th27;
  take H;
  thus H = F-MSF(the carrier of S1, the Sorts of A1);
  let o be OperSymbol of S1;
  assume
A2: Args(o,A1) <> {};
  per cases by Th15;
  suppose
    o`1 = 1;
    then consider a being Object of C1 such that
A3: o = idsym(a) by Th16;
    let x be Element of Args(o,A1);
A4: Args(G.o,A2) = Args(o,B1) by A1,INSTALG1:24;
A5: G.o = idsym(F.a) by A3,Th21;
    then Args(G.o,A2) = {{}} by Th24;
    then
A6: H#x = {} by A4,TARSKI:def 1;
    reconsider h = id a as Morphism of a,a;
    dom id a = a & cod id a = a by CAT_1:58;
    then
A7: id a in Hom(a,a);
    Args(o,A1) = {{}} by A3,Th24;
    then x = {} by TARSKI:def 1;
    hence
    (H.(the_result_sort_of o)).(Den(o,A1).x) = (H.(the_result_sort_of o))
    .h by A3,Def13
      .= (H.homsym(a,a)).h by A3,Def3
      .= (F|((the Sorts of A1).homsym(a,a))).h by Def1
      .= (F|Hom(a,a)).h by Def13
      .= hom(F,a,a).h
      .= F.h by A7,CAT_1:88
      .= id (F.a) by CAT_1:71
      .= Den(G.o,A2).(H#x) by A5,A6,Def13
      .= Den(o,B1).(H#x) by Th23,INSTALG1:23;
  end;
  suppose
A8: o`1 = 2;
    let x be Element of Args(o,A1);
    consider a,b,c being Object of C1 such that
A9: o = compsym(a,b,c) by A8,Th17;
A10: G.o = compsym(F.a,F.b,F.c) by A9,Th22;
    consider g,h being Morphism of C1 such that
A11: x = <*g,h*> and
A12: dom h = a and
A13: cod h = b and
A14: dom g = b and
A15: cod g = c by A2,A9,Th28;
A16: g in Hom(b,c) & h in Hom(a,b) by A12,A13,A14,A15;
    dom (g(*)h) = a & cod (g(*)h) = c by A12,A13,A14,A15,CAT_1:17;
    then
A17: g(*)h in Hom(a,c);
    then reconsider gh = g(*)h as Morphism of a,c by CAT_1:def 5;
A18: dom (F.h) = F.a & cod (F.h) = F.b by A12,A13,CAT_1:72;
A19: dom (F.g) = F.b & cod (F.g) = F.c by A14,A15,CAT_1:72;
    thus (H.(the_result_sort_of o)).(Den(o,A1).x) = (H.(the_result_sort_of o))
    .gh by A9,A11,A12,A13,A14,A15,Def13
      .= (H.homsym(a,c)).gh by A9,Def3
      .= (F|((the Sorts of A1).homsym(a,c))).gh by Def1
      .= (F|Hom(a,c)).gh by Def13
      .= hom(F,a,c).gh
      .= F.gh by A17,CAT_1:88
      .= (F.g)(*)(F.h) by A13,A14,CAT_1:64
      .= Den(G.o,A2).<*F.g,F.h*> by A10,A18,A19,Def13
      .= Den(G.o,A2).(H#x) by A9,A11,A16,Th29
      .= Den(o,B1).(H#x) by Th23,INSTALG1:23;
  end;
end;