:: CATALG_1 semantic presentation

begin

definition
let I be set ;
let A, f be Function;
funcf -MSF (I,A) ->  ManySortedFunction of I means :Def1: :: CATALG_1:def 1
 for i being set st i in I holds
it . i = f | (A . i);
existence
 ex b1 being ManySortedFunction of I st
for i being set st i in I holds
b1 . i = f | (A . i)
proof
deffunc H1( set ) ->  set = f | (A . $1);
consider F being ManySortedSet of I such that
A1: for i being set st i in I holds
F . i = H1(i) from PBOOLE:sch_4();
 F is Function-yielding
proof
let x be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not x in proj1 F or F . x is set )
assume  x in dom F ; ::_thesis: F . x is set
then  x in I ;
then  F . x = f | (A . x) by A1;
hence  F . x is set ; ::_thesis: verum
end;
hence  ex b1 being ManySortedFunction of I st
for i being set st i in I holds
b1 . i = f | (A . i) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being ManySortedFunction of I st ( for i being set st i in I holds
b1 . i = f | (A . i) ) & ( for i being set st i in I holds
b2 . i = f | (A . i) ) holds
b1 = b2
proof
let g1, g2 be ManySortedFunction of I; ::_thesis: ( ( for i being set st i in I holds
g1 . i = f | (A . i) ) & ( for i being set st i in I holds
g2 . i = f | (A . i) ) implies g1 = g2 )
assume 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) ; ::_thesis: g1 = g2
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
g1_._i_=_g2_._i
let i be set ; ::_thesis: ( i in I implies g1 . i = g2 . i )
assume A4: i in I ; ::_thesis: g1 . i = g2 . i
then  g1 . i = f | (A . i) by A2;
hence  g1 . i = g2 . i by A3, A4; ::_thesis: verum
end;
hence  g1 = g2 by PBOOLE:3; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines -MSF CATALG_1:def_1_:_
 for I being set
for A, f being Function
for b4 being ManySortedFunction of I holds
( b4 = f -MSF (I,A) iff for i being set st i in I holds
b4 . i = f | (A . i) );

theorem :: CATALG_1:1
for I being set
for A being ManySortedSet of I holds (id (Union A)) -MSF (I,A) = id A
proof
let I be set ; ::_thesis: for A being ManySortedSet of I holds (id (Union A)) -MSF (I,A) = id A
let A be ManySortedSet of I; ::_thesis: (id (Union A)) -MSF (I,A) = id A
set f = id (Union A);
set F = (id (Union A)) -MSF (I,A);
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
((id_(Union_A))_-MSF_(I,A))_._i_=_(id_A)_._i
let i be set ; ::_thesis: ( i in I implies ((id (Union A)) -MSF (I,A)) . i = (id A) . i )
A1: Union A = union (rng A) by CARD_3:def_4;
assume A2: i in I ; ::_thesis: ((id (Union A)) -MSF (I,A)) . i = (id A) . i
then  i in dom A by PARTFUN1:def_2;
then A3: A . i in rng A by FUNCT_1:def_3;
 ( ((id (Union A)) -MSF (I,A)) . i = (id (Union A)) | (A . i) & (id A) . i = id (A . i) ) by A2, Def1, MSUALG_3:def_1;
hence  ((id (Union A)) -MSF (I,A)) . i = (id A) . i by A3, A1, FUNCT_3:1, ZFMISC_1:74; ::_thesis: verum
end;
hence  (id (Union A)) -MSF (I,A) = id A by PBOOLE:3; ::_thesis: verum
end;

theorem :: CATALG_1:2
for I being set
for 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 ; ::_thesis: for 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))
let A, B be ManySortedSet of I; ::_thesis: 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))
let f, g be Function; ::_thesis: ( rngs (f -MSF (I,A)) c= B implies (g * f) -MSF (I,A) = (g -MSF (I,B)) ** (f -MSF (I,A)) )
assume A1: rngs (f -MSF (I,A)) c= B ; ::_thesis: (g * f) -MSF (I,A) = (g -MSF (I,B)) ** (f -MSF (I,A))
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__::_thesis:_for_i_being_set_st_i_in_I_holds_
((g_*_f)_-MSF_(I,A))_._i_=_((g_-MSF_(I,B))_**_(f_-MSF_(I,A)))_._i
let i be set ; ::_thesis: ( i in I implies ((g * f) -MSF (I,A)) . i = ((g -MSF (I,B)) ** (f -MSF (I,A))) . i )
assume A5: i in I ; ::_thesis: ((g * f) -MSF (I,A)) . i = ((g -MSF (I,B)) ** (f -MSF (I,A))) . 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, RELAT_1: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; ::_thesis: verum
end;
 dom ((g * f) -MSF (I,A)) = I by PARTFUN1:def_2;
hence  (g * f) -MSF (I,A) = (g -MSF (I,B)) ** (f -MSF (I,A)) by A3, A4, FUNCT_1:2; ::_thesis: verum
end;

theorem :: CATALG_1:3
for f being Function
for 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; ::_thesis: for 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
let I be set ; ::_thesis: 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
let A, B be ManySortedSet of I; ::_thesis: ( ( for i being set st i in I holds
( A . i c= dom f & f .: (A . i) c= B . i ) ) implies f -MSF (I,A) is ManySortedFunction of A,B )
assume A1: for i being set st i in I holds
( A . i c= dom f & f .: (A . i) c= B . i ) ; ::_thesis: f -MSF (I,A) is ManySortedFunction of A,B
let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in I or (f -MSF (I,A)) . i is Element of bool [:(A . i),(B . i):] )
assume A2: i in I ; ::_thesis: (f -MSF (I,A)) . i is Element of bool [:(A . i),(B . 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  (f -MSF (I,A)) . i is Element of bool [:(A . i),(B . i):] by A4, FUNCT_2:2; ::_thesis: verum
end;

Lm1: now__::_thesis:_for_x,_y_being_set_st_<*x*>_=_<*y*>_holds_
x_=_y
let x, y be set ; ::_thesis: ( <*x*> = <*y*> implies x = y )
assume  <*x*> = <*y*> ; ::_thesis: x = y
then  <*x*> . 1 = y by FINSEQ_1:40;
hence  x = y by FINSEQ_1:40; ::_thesis: verum
end;

definition
let S be non empty ManySortedSign ;
let A be MSAlgebra over S;
attrA is empty  means :Def2: :: CATALG_1:def 2
 the Sorts of A is V3();
end;

:: deftheorem Def2 defines empty CATALG_1:def_2_:_
 for S being non empty ManySortedSign
for A being MSAlgebra over S holds
( A is empty iff the Sorts of A is V3() );

registration
let S be non empty ManySortedSign ;
cluster non-empty  ->  non empty for MSAlgebra over S;
coherence
 for b1 being MSAlgebra over S st b1 is non-empty holds
not b1 is empty
proof
let A be MSAlgebra over S; ::_thesis: ( A is non-empty implies not A is empty )
assume  the Sorts of A is V2() ; :: according to MSUALG_1:def_3 ::_thesis: not A is empty
hence  the Sorts of A is V3() ; :: according to CATALG_1:def_2 ::_thesis: verum
end;
end;

registration
let S be non empty non void ManySortedSign ;
cluster strict non-empty disjoint_valued for MSAlgebra over S;
existence
 ex b1 being MSAlgebra over S st
( b1 is strict & b1 is non-empty & b1 is disjoint_valued )
proof
set X = the V2() ManySortedSet of the carrier of S;
take  FreeMSA the V2() ManySortedSet of the carrier of S ; ::_thesis: ( FreeMSA the V2() ManySortedSet of the carrier of S is strict & FreeMSA the V2() ManySortedSet of the carrier of S is non-empty & FreeMSA the V2() ManySortedSet of the carrier of S is disjoint_valued )
thus  ( FreeMSA the V2() ManySortedSet of the carrier of S is strict & FreeMSA the V2() ManySortedSet of the carrier of S is non-empty & FreeMSA the V2() ManySortedSet of the carrier of S is disjoint_valued ) ; ::_thesis: verum
end;
end;

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

registration
cluster Relation-like non empty-yielding Function-like for set ;
existence
 not for b1 being Function holds b1 is empty-yielding
proof
set S = the non empty non void ManySortedSign ;
set A = the non empty MSAlgebra over the non empty non void ManySortedSign ;
take  the Sorts of the non empty MSAlgebra over the non empty non void ManySortedSign ; ::_thesis: not the Sorts of the non empty MSAlgebra over the non empty non void ManySortedSign is empty-yielding
thus  not the Sorts of the non empty MSAlgebra over the non empty non void ManySortedSign is empty-yielding ; ::_thesis: verum
end;
end;

begin

definition
let A be set ;
func CatSign A ->  strict ManySortedSign  means :Def3: :: CATALG_1:def 3
( 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
 ex b1 being strict ManySortedSign st
( the carrier of b1 = [:{0},(2 -tuples_on A):] & the carrier' of b1 = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for a being set st a in A holds
( the Arity of b1 . [1,<*a*>] = {} & the ResultSort of b1 . [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 b1 . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of b1 . [2,<*a,b,c*>] = [0,<*a,c*>] ) ) )
proof
defpred S1[ 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 S2[ 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):] holds
ex y being set st
( y in [:{0},(2 -tuples_on A):] * & S2[x,y] )
proof
let x be set ; ::_thesis: ( x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] implies ex y being set st
( y in [:{0},(2 -tuples_on A):] * & S2[x,y] ) )
assume A2: x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] ; ::_thesis: ex y being set st
( y in [:{0},(2 -tuples_on A):] * & S2[x,y] )
percases ( x in [:{1},(1 -tuples_on A):] or x in [:{2},(3 -tuples_on A):] ) by A2, XBOOLE_0:def_3;
supposeA3: x in [:{1},(1 -tuples_on A):] ; ::_thesis: ex y being set st
( y in [:{0},(2 -tuples_on A):] * & S2[x,y] )
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 = {} ; ::_thesis: ( y in [:{0},(2 -tuples_on A):] * & S2[x,y] )
thus  y in [:{0},(2 -tuples_on A):] * by FINSEQ_1:49; ::_thesis: S2[x,y]
consider s being Element of A *  such that
A5: x `2 = s and
A6: len s = 1 by A4;
take y1 = s . 1; ::_thesis: ex y2, y3 being set st
( y1 in A & y2 in A & y3 in A & ( ( x = [1,<*y1*>] & y = {} ) or ( x = [2,<*y1,y2,y3*>] & y = <*[0,<*y2,y3*>],[0,<*y1,y2*>]*> ) ) )
take y2 = s . 1; ::_thesis: ex y3 being set st
( y1 in A & y2 in A & y3 in A & ( ( x = [1,<*y1*>] & y = {} ) or ( x = [2,<*y1,y2,y3*>] & y = <*[0,<*y2,y3*>],[0,<*y1,y2*>]*> ) ) )
take y3 = s . 1; ::_thesis: ( y1 in A & y2 in A & y3 in A & ( ( x = [1,<*y1*>] & y = {} ) or ( x = [2,<*y1,y2,y3*>] & y = <*[0,<*y2,y3*>],[0,<*y1,y2*>]*> ) ) )
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 ) ; ::_thesis: ( ( x = [1,<*y1*>] & y = {} ) or ( x = [2,<*y1,y2,y3*>] & y = <*[0,<*y2,y3*>],[0,<*y1,y2*>]*> ) )
 x `1 in {1} by A3, MCART_1:10;
then  x `1 = 1 by TARSKI:def_1;
hence  ( ( x = [1,<*y1*>] & y = {} ) or ( x = [2,<*y1,y2,y3*>] & y = <*[0,<*y2,y3*>],[0,<*y1,y2*>]*> ) ) by A3, A5, A7, MCART_1:21; ::_thesis: verum
end;
supposeA8: x in [:{2},(3 -tuples_on A):] ; ::_thesis: ex y being set st
( y in [:{0},(2 -tuples_on A):] * & S2[x,y] )
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;
set y2 = s . 2;
set y3 = s . 3;
A11: s = <*(s . 1),(s . 2),(s . 3)*> by A10, FINSEQ_1:45;
then A12: rng s = {(s . 1),(s . 2),(s . 3)} by FINSEQ_2:128;
then reconsider B = A as non empty set ;
take y = <*[0,<*(s . 2),(s . 3)*>],[0,<*(s . 1),(s . 2)*>]*>; ::_thesis: ( y in [:{0},(2 -tuples_on A):] * & S2[x,y] )
A13: s . 2 in {(s . 1),(s . 2),(s . 3)} by ENUMSET1:def_1;
A14: s . 1 in {(s . 1),(s . 2),(s . 3)} by ENUMSET1:def_1;
then A15: ( 0 in {0} & <*(s . 1),(s . 2)*> in 2 -tuples_on B ) by A13, A12, FINSEQ_2:101, TARSKI:def_1;
A16: s . 3 in {(s . 1),(s . 2),(s . 3)} by ENUMSET1:def_1;
then  <*(s . 2),(s . 3)*> in 2 -tuples_on B by A13, A12, FINSEQ_2:101;
then reconsider z1 = [0,<*(s . 2),(s . 3)*>], z2 = [0,<*(s . 1),(s . 2)*>] 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; ::_thesis: S2[x,y]
take  s . 1 ; ::_thesis: ex y2, y3 being set st
( s . 1 in A & y2 in A & y3 in A & ( ( x = [1,<*(s . 1)*>] & y = {} ) or ( x = [2,<*(s . 1),y2,y3*>] & y = <*[0,<*y2,y3*>],[0,<*(s . 1),y2*>]*> ) ) )
take  s . 2 ; ::_thesis: ex y3 being set st
( s . 1 in A & s . 2 in A & y3 in A & ( ( x = [1,<*(s . 1)*>] & y = {} ) or ( x = [2,<*(s . 1),(s . 2),y3*>] & y = <*[0,<*(s . 2),y3*>],[0,<*(s . 1),(s . 2)*>]*> ) ) )
take  s . 3 ; ::_thesis: ( s . 1 in A & s . 2 in A & s . 3 in A & ( ( x = [1,<*(s . 1)*>] & y = {} ) or ( x = [2,<*(s . 1),(s . 2),(s . 3)*>] & y = <*[0,<*(s . 2),(s . 3)*>],[0,<*(s . 1),(s . 2)*>]*> ) ) )
thus  ( s . 1 in A & s . 2 in A & s . 3 in A ) by A14, A13, A16, A12; ::_thesis: ( ( x = [1,<*(s . 1)*>] & y = {} ) or ( x = [2,<*(s . 1),(s . 2),(s . 3)*>] & y = <*[0,<*(s . 2),(s . 3)*>],[0,<*(s . 1),(s . 2)*>]*> ) )
 x `1 in {2} by A8, MCART_1:10;
then  x `1 = 2 by TARSKI:def_1;
hence  ( ( x = [1,<*(s . 1)*>] & y = {} ) or ( x = [2,<*(s . 1),(s . 2),(s . 3)*>] & y = <*[0,<*(s . 2),(s . 3)*>],[0,<*(s . 1),(s . 2)*>]*> ) ) by A8, A9, A11, MCART_1:21; ::_thesis: verum
end;
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
S2[x,Ar . x] from FUNCT_1:sch_5(A1);
reconsider Ar = 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):] holds
ex y being set st
( y in [:{0},(2 -tuples_on A):] & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] implies ex y being set st
( y in [:{0},(2 -tuples_on A):] & S1[x,y] ) )
assume A20: x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] ; ::_thesis: ex y being set st
( y in [:{0},(2 -tuples_on A):] & S1[x,y] )
percases ( x in [:{1},(1 -tuples_on A):] or x in [:{2},(3 -tuples_on A):] ) by A20, XBOOLE_0:def_3;
supposeA21: x in [:{1},(1 -tuples_on A):] ; ::_thesis: ex y being set st
( y in [:{0},(2 -tuples_on A):] & S1[x,y] )
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;
set y2 = s . 1;
set y3 = s . 1;
A24: s = <*(s . 1)*> by A23, FINSEQ_1:40;
then A25: ( s . 1 in {(s . 1)} & rng s = {(s . 1)} ) by FINSEQ_1:39, TARSKI:def_1;
take y = [0,<*(s . 1),(s . 1)*>]; ::_thesis: ( y in [:{0},(2 -tuples_on A):] & S1[x,y] )
reconsider B = A as non empty set by A24;
reconsider y1 = s . 1 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; ::_thesis: S1[x,y]
take  y1 ; ::_thesis: ex y2, y3 being set st
( y1 in A & y2 in A & y3 in A & ( ( x = [1,<*y1*>] & y = [0,<*y1,y1*>] ) or ( x = [2,<*y1,y2,y3*>] & y = [0,<*y1,y3*>] ) ) )
take  s . 1 ; ::_thesis: ex y3 being set st
( y1 in A & s . 1 in A & y3 in A & ( ( x = [1,<*y1*>] & y = [0,<*y1,y1*>] ) or ( x = [2,<*y1,(s . 1),y3*>] & y = [0,<*y1,y3*>] ) ) )
take  s . 1 ; ::_thesis: ( y1 in A & s . 1 in A & s . 1 in A & ( ( x = [1,<*y1*>] & y = [0,<*y1,y1*>] ) or ( x = [2,<*y1,(s . 1),(s . 1)*>] & y = [0,<*y1,(s . 1)*>] ) ) )
thus  ( y1 in A & s . 1 in A & s . 1 in A ) by A25; ::_thesis: ( ( x = [1,<*y1*>] & y = [0,<*y1,y1*>] ) or ( x = [2,<*y1,(s . 1),(s . 1)*>] & y = [0,<*y1,(s . 1)*>] ) )
 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,(s . 1),(s . 1)*>] & y = [0,<*y1,(s . 1)*>] ) ) by A21, A22, A24, MCART_1:21; ::_thesis: verum
end;
supposeA26: x in [:{2},(3 -tuples_on A):] ; ::_thesis: ex y being set st
( y in [:{0},(2 -tuples_on A):] & S1[x,y] )
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;
set y2 = s . 2;
set y3 = s . 3;
A29: s = <*(s . 1),(s . 2),(s . 3)*> by A28, FINSEQ_1:45;
then A30: rng s = {(s . 1),(s . 2),(s . 3)} by FINSEQ_2:128;
then reconsider B = A as non empty set ;
take y = [0,<*(s . 1),(s . 3)*>]; ::_thesis: ( y in [:{0},(2 -tuples_on A):] & S1[x,y] )
A31: ( s . 1 in {(s . 1),(s . 2),(s . 3)} & s . 3 in {(s . 1),(s . 2),(s . 3)} ) by ENUMSET1:def_1;
then  ( 0 in {0} & <*(s . 1),(s . 3)*> 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; ::_thesis: S1[x,y]
take  s . 1 ; ::_thesis: ex y2, y3 being set st
( s . 1 in A & y2 in A & y3 in A & ( ( x = [1,<*(s . 1)*>] & y = [0,<*(s . 1),(s . 1)*>] ) or ( x = [2,<*(s . 1),y2,y3*>] & y = [0,<*(s . 1),y3*>] ) ) )
take  s . 2 ; ::_thesis: ex y3 being set st
( s . 1 in A & s . 2 in A & y3 in A & ( ( x = [1,<*(s . 1)*>] & y = [0,<*(s . 1),(s . 1)*>] ) or ( x = [2,<*(s . 1),(s . 2),y3*>] & y = [0,<*(s . 1),y3*>] ) ) )
take  s . 3 ; ::_thesis: ( s . 1 in A & s . 2 in A & s . 3 in A & ( ( x = [1,<*(s . 1)*>] & y = [0,<*(s . 1),(s . 1)*>] ) or ( x = [2,<*(s . 1),(s . 2),(s . 3)*>] & y = [0,<*(s . 1),(s . 3)*>] ) ) )
 s . 2 in {(s . 1),(s . 2),(s . 3)} by ENUMSET1:def_1;
hence  ( s . 1 in A & s . 2 in A & s . 3 in A ) by A31, A30; ::_thesis: ( ( x = [1,<*(s . 1)*>] & y = [0,<*(s . 1),(s . 1)*>] ) or ( x = [2,<*(s . 1),(s . 2),(s . 3)*>] & y = [0,<*(s . 1),(s . 3)*>] ) )
 x `1 in {2} by A26, MCART_1:10;
then  x `1 = 2 by TARSKI:def_1;
hence  ( ( x = [1,<*(s . 1)*>] & y = [0,<*(s . 1),(s . 1)*>] ) or ( x = [2,<*(s . 1),(s . 2),(s . 3)*>] & y = [0,<*(s . 1),(s . 3)*>] ) ) by A26, A27, A29, MCART_1:21; ::_thesis: verum
end;
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
S1[x,R . x] from FUNCT_1:sch_5(A19);
reconsider R = 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 #); ::_thesis: ( the carrier of S = [:{0},(2 -tuples_on A):] & the carrier' of S = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for a being set st a in A holds
( the Arity of S . [1,<*a*>] = {} & the ResultSort of S . [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 S . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of S . [2,<*a,b,c*>] = [0,<*a,c*>] ) ) )
thus  the carrier of S = [:{0},(2 -tuples_on A):] ; ::_thesis: ( the carrier' of S = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for a being set st a in A holds
( the Arity of S . [1,<*a*>] = {} & the ResultSort of S . [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 S . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of S . [2,<*a,b,c*>] = [0,<*a,c*>] ) ) )
thus  the carrier' of S = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] ; ::_thesis: ( ( for a being set st a in A holds
( the Arity of S . [1,<*a*>] = {} & the ResultSort of S . [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 S . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of S . [2,<*a,b,c*>] = [0,<*a,c*>] ) ) )
hereby  ::_thesis: for a, b, c being set st a in A & b in A & c in A holds
( the Arity of S . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of S . [2,<*a,b,c*>] = [0,<*a,c*>] )
let a be set ; ::_thesis: ( a in A implies ( the Arity of S . [1,<*a*>] = {} & the ResultSort of S . [1,<*a*>] = [0,<*a,a*>] ) )
assume A34: a in A ; ::_thesis: ( the Arity of S . [1,<*a*>] = {} & the ResultSort of S . [1,<*a*>] = [0,<*a,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; ::_thesis: the ResultSort of S . [1,<*a*>] = [0,<*a,a*>]
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; ::_thesis: verum
end;
let a, b, c be set ; ::_thesis: ( a in A & b in A & c in A implies ( the Arity of S . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of S . [2,<*a,b,c*>] = [0,<*a,c*>] ) )
assume that
A38: a in A and
A39: ( b in A & c in A ) ; ::_thesis: ( the Arity of S . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of S . [2,<*a,b,c*>] = [0,<*a,c*>] )
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; ::_thesis: the ResultSort of S . [2,<*a,b,c*>] = [0,<*a,c*>]
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  the ResultSort of S . [2,<*a,b,c*>] = [0,<*a,c*>] by A46, A47, A48, FINSEQ_1:45, XTUPLE_0:1; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being strict ManySortedSign st the carrier of b1 = [:{0},(2 -tuples_on A):] & the carrier' of b1 = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for a being set st a in A holds
( the Arity of b1 . [1,<*a*>] = {} & the ResultSort of b1 . [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 b1 . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of b1 . [2,<*a,b,c*>] = [0,<*a,c*>] ) ) & the carrier of b2 = [:{0},(2 -tuples_on A):] & the carrier' of b2 = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for a being set st a in A holds
( the Arity of b2 . [1,<*a*>] = {} & the ResultSort of b2 . [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 b2 . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of b2 . [2,<*a,b,c*>] = [0,<*a,c*>] ) ) holds
b1 = b2;
proof
let S1, S2 be strict ManySortedSign ; ::_thesis: ( the carrier of S1 = [:{0},(2 -tuples_on A):] & the carrier' of S1 = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for a being set st a in A holds
( the Arity of S1 . [1,<*a*>] = {} & the ResultSort of S1 . [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 S1 . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of S1 . [2,<*a,b,c*>] = [0,<*a,c*>] ) ) & the carrier of S2 = [:{0},(2 -tuples_on A):] & the carrier' of S2 = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for a being set st a in A holds
( the Arity of S2 . [1,<*a*>] = {} & the ResultSort of S2 . [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 S2 . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of S2 . [2,<*a,b,c*>] = [0,<*a,c*>] ) ) implies S1 = S2 )
assume 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*>] ) ; ::_thesis: S1 = S2
A57: now__::_thesis:_for_x_being_set_st_x_in_[:{1},(1_-tuples_on_A):]_\/_[:{2},(3_-tuples_on_A):]_holds_
the_Arity_of_S1_._x_=_the_Arity_of_S2_._x
let x be set ; ::_thesis: ( x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] implies the Arity of S1 . x = the Arity of S2 . x )
assume  x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] ; ::_thesis: the Arity of S1 . x = the Arity of S2 . x
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__::_thesis:_(_x_`2_in_3_-tuples_on_A_implies_the_Arity_of_S1_._[2,(x_`2)]_=_the_Arity_of_S2_._[2,(x_`2)]_)
assume  x `2 in 3 -tuples_on A ; ::_thesis: the Arity of S1 . [2,(x `2)] = the Arity of S2 . [2,(x `2)]
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 ; ::_thesis: verum
end;
A62: now__::_thesis:_(_x_`2_in_1_-tuples_on_A_implies_the_Arity_of_S1_._[1,(x_`2)]_=_the_Arity_of_S2_._[1,(x_`2)]_)
assume  x `2 in 1 -tuples_on A ; ::_thesis: the Arity of S1 . [1,(x `2)] = the Arity of S2 . [1,(x `2)]
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 ;
::_thesis: verum
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; ::_thesis: verum
end;
A64: now__::_thesis:_for_x_being_set_st_x_in_[:{1},(1_-tuples_on_A):]_\/_[:{2},(3_-tuples_on_A):]_holds_
the_ResultSort_of_S1_._x_=_the_ResultSort_of_S2_._x
let x be set ; ::_thesis: ( x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] implies the ResultSort of S1 . x = the ResultSort of S2 . x )
assume  x in [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] ; ::_thesis: the ResultSort of S1 . x = the ResultSort of S2 . x
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__::_thesis:_(_x_`2_in_3_-tuples_on_A_implies_the_ResultSort_of_S1_._[2,(x_`2)]_=_the_ResultSort_of_S2_._[2,(x_`2)]_)
assume  x `2 in 3 -tuples_on A ; ::_thesis: the ResultSort of S1 . [2,(x `2)] = the ResultSort of S2 . [2,(x `2)]
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 ; ::_thesis: verum
end;
A69: now__::_thesis:_(_x_`2_in_1_-tuples_on_A_implies_the_ResultSort_of_S1_._[1,(x_`2)]_=_the_ResultSort_of_S2_._[1,(x_`2)]_)
assume  x `2 in 1 -tuples_on A ; ::_thesis: the ResultSort of S1 . [1,(x `2)] = the ResultSort of S2 . [1,(x `2)]
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 ; ::_thesis: verum
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; ::_thesis: verum
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__::_thesis:_(_[:{0},(2_-tuples_on_A):]_=_{}_implies_[:{1},(1_-tuples_on_A):]_\/_[:{2},(3_-tuples_on_A):]_=_{}_)
assume  [:{0},(2 -tuples_on A):] = {} ; ::_thesis: [:{1},(1 -tuples_on A):] \/ [:{2},(3 -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; ::_thesis: verum
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  S1 = S2 by A49, A50, A53, A54, A71, A64, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines CatSign CATALG_1:def_3_:_
 for A being set
for b2 being strict ManySortedSign holds
( b2 = CatSign A iff ( the carrier of b2 = [:{0},(2 -tuples_on A):] & the carrier' of b2 = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for a being set st a in A holds
( the Arity of b2 . [1,<*a*>] = {} & the ResultSort of b2 . [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 b2 . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of b2 . [2,<*a,b,c*>] = [0,<*a,c*>] ) ) ) );

registration
let A be set ;
cluster CatSign A ->  strict feasible ;
coherence
 CatSign A is feasible
proof
assume  the carrier of (CatSign A) = {} ; :: according to INSTALG1:def_1 ::_thesis: 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  the carrier' of (CatSign A) = {} by Def3; ::_thesis: verum
end;
end;

registration
let A be non empty set ;
cluster CatSign A ->  non empty non void strict ;
coherence
 ( not CatSign A is empty & not CatSign A is void )
proof
 the carrier of (CatSign A) = [:{0},(2 -tuples_on A):] by Def3;
hence  not the carrier of (CatSign A) is empty ; :: according to STRUCT_0:def_1 ::_thesis: not CatSign A is void
 the carrier' of (CatSign A) = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] by Def3;
hence  not the carrier' of (CatSign A) is empty ; :: according to STRUCT_0:def_13 ::_thesis: verum
end;
end;

definition
mode Signature is feasible ManySortedSign ;
end;

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

:: deftheorem Def4 defines Categorial CATALG_1:def_4_:_
 for S being Signature holds
( S is Categorial iff ex A being set st
( CatSign A is Subsignature of S & the carrier of S = [:{0},(2 -tuples_on A):] ) );

registration
cluster non empty feasible Categorial  ->  non empty non void for ManySortedSign ;
coherence
 for b1 being non empty Signature st b1 is Categorial holds
not b1 is void
proof
let S be non empty Signature; ::_thesis: ( S is Categorial implies not S is void )
given A being set  such that A1: CatSign A is Subsignature of S and
A2: the carrier of S = [:{0},(2 -tuples_on A):] ; :: according to CATALG_1:def_4 ::_thesis: not S is void
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
 the SortSymbol of 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  not the carrier' of S is empty ; :: according to STRUCT_0:def_13 ::_thesis: verum
end;
end;

registration
cluster non empty strict feasible Categorial for ManySortedSign ;
existence
 ex b1 being Signature st
( b1 is Categorial & not b1 is empty & b1 is strict )
proof
take S = CatSign {{}}; ::_thesis: ( S is Categorial & not S is empty & S is strict )
thus  S is Categorial ::_thesis: ( not S is empty & S is strict )
proof
take  {{}} ; :: according to CATALG_1:def_4 ::_thesis: ( CatSign {{}} is Subsignature of S & the carrier of S = [:{0},(2 -tuples_on {{}}):] )
thus  ( CatSign {{}} is Subsignature of S & the carrier of S = [:{0},(2 -tuples_on {{}}):] ) by Def3, INSTALG1:15; ::_thesis: verum
end;
thus  ( not S is empty & S is strict ) ; ::_thesis: verum
end;
end;

definition
mode CatSignature is Categorial Signature;
end;

definition
let A be set ;
mode CatSignature of A ->  Signature means :Def5: :: CATALG_1:def 5
( CatSign A is Subsignature of it & the carrier of it = [:{0},(2 -tuples_on A):] );
existence
 ex b1 being Signature st
( CatSign A is Subsignature of b1 & the carrier of b1 = [:{0},(2 -tuples_on A):] )
proof
set S = CatSign A;
 ( CatSign A is Subsignature of CatSign A & the carrier of (CatSign A) = [:{0},(2 -tuples_on A):] ) by Def3, INSTALG1:15;
then reconsider S = CatSign A as CatSignature by Def4;
take  S ; ::_thesis: ( CatSign A is Subsignature of S & the carrier of S = [:{0},(2 -tuples_on A):] )
thus  ( CatSign A is Subsignature of S & the carrier of S = [:{0},(2 -tuples_on A):] ) by Def3, INSTALG1:15; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines CatSignature CATALG_1:def_5_:_
 for A being set
for b2 being Signature holds
( b2 is CatSignature of A iff ( CatSign A is Subsignature of b2 & the carrier of b2 = [:{0},(2 -tuples_on A):] ) );

theorem :: CATALG_1:4
for A1, A2 being set
for S being CatSignature of A1 st S is CatSignature of A2 holds
A1 = A2
proof
let A1, A2 be set ; ::_thesis: for S being CatSignature of A1 st S is CatSignature of A2 holds
A1 = A2
let S be CatSignature of A1; ::_thesis: ( S is CatSignature of A2 implies A1 = A2 )
assume that
 CatSign A2 is Subsignature of S and
A1: the carrier of S = [:{0},(2 -tuples_on A2):] ; :: according to CATALG_1:def_5 ::_thesis: A1 = 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  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: A2 c= A1
let x be set ; ::_thesis: ( x in A1 implies x in A2 )
assume  x in A1 ; ::_thesis: x in A2
then  <*x,x*> in 2 -tuples_on A1 by FINSEQ_2:137;
hence  x in A2 by A3, FINSEQ_2:138; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A2 or x in A1 )
assume  x in A2 ; ::_thesis: x in A1
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  x in A1 by A4, FINSEQ_2:138; ::_thesis: verum
end;

registration
let A be set ;
cluster  ->  Categorial for CatSignature of A;
coherence
 for b1 being CatSignature of A holds b1 is Categorial
proof
let S be CatSignature of A; ::_thesis: S is Categorial
take  A ; :: according to CATALG_1:def_4 ::_thesis: ( CatSign A is Subsignature of S & the carrier of S = [:{0},(2 -tuples_on A):] )
thus  ( CatSign A is Subsignature of S & the carrier of S = [:{0},(2 -tuples_on A):] ) by Def5; ::_thesis: verum
end;
end;

registration
let A be non empty set ;
cluster  ->  non empty for CatSignature of A;
coherence
 for b1 being CatSignature of A holds not b1 is empty
proof
let S be CatSignature of A; ::_thesis: not S is empty
 CatSign A is Subsignature of S by Def5;
then  the carrier of (CatSign A) c= the carrier of S by INSTALG1:10;
hence  not the carrier of S is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;

registration
let A be set ;
cluster strict feasible Categorial for CatSignature of A;
existence
 ex b1 being CatSignature of A st b1 is strict
proof
set S = CatSign A;
 ( CatSign A is Subsignature of CatSign A & the carrier of (CatSign A) = [:{0},(2 -tuples_on A):] ) by Def3, INSTALG1:15;
then  CatSign A is CatSignature of A by Def5;
hence  ex b1 being CatSignature of A st b1 is strict ; ::_thesis: verum
end;
end;

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

definition
let S be ManySortedSign ;
func underlay S ->  set  means :Def6: :: CATALG_1:def 6
 for x being set holds
( x in it iff ex a being set ex f being Function st
( [a,f] in the carrier of S \/ the carrier' of S & x in rng f ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ex a being set ex f being Function st
( [a,f] in the carrier of S \/ the carrier' of S & x in rng f ) )
proof
set A = the carrier of S \/ the carrier' of S;
take X = proj2 (union (SubFuncs (proj2 ( the carrier of S \/ the carrier' of S)))); ::_thesis: for x being set holds
( x in X iff ex a being set ex f being Function st
( [a,f] in the carrier of S \/ the carrier' of S & x in rng f ) )
let x be set ; ::_thesis: ( x in X iff ex a being set ex f being Function st
( [a,f] in the carrier of S \/ the carrier' of S & x in rng f ) )
hereby  ::_thesis: ( ex a being set ex f being Function st
( [a,f] in the carrier of S \/ the carrier' of S & x in rng f ) implies x in X )
assume  x in X ; ::_thesis: ex c being set ex b being Function st
( [c,b] in the carrier of S \/ the carrier' of S & x in rng b )
then consider a being set  such that
A1: [a,x] in union (SubFuncs (proj2 ( the carrier of S \/ the carrier' of S))) by XTUPLE_0:def_13;
consider b being set  such that
A2: [a,x] in b and
A3: b in SubFuncs (proj2 ( the carrier of S \/ the carrier' of S)) by A1, TARSKI:def_4;
reconsider b = b as Function by A3, FUNCT_6:def_1;
 b in proj2 ( the carrier of S \/ the carrier' of S) by A3, FUNCT_6:def_1;
then consider c being set  such that
A4: [c,b] in the carrier of S \/ the carrier' of S by XTUPLE_0:def_13;
take c = c; ::_thesis: ex b being Function st
( [c,b] in the carrier of S \/ the carrier' of S & x in rng b )
take b = b; ::_thesis: ( [c,b] in the carrier of S \/ the carrier' of S & x in rng b )
thus  ( [c,b] in the carrier of S \/ the carrier' of S & x in rng b ) by A2, A4, XTUPLE_0:def_13; ::_thesis: verum
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 ; ::_thesis: x in X
consider b being set  such that
A7: [b,x] in f by A6, XTUPLE_0:def_13;
 f in proj2 ( the carrier of S \/ the carrier' of S) by A5, XTUPLE_0:def_13;
then  f in SubFuncs (proj2 ( the carrier of S \/ the carrier' of S)) by FUNCT_6:def_1;
then  [b,x] in union (SubFuncs (proj2 ( the carrier of S \/ the carrier' of S))) by A7, TARSKI:def_4;
hence  x in X by XTUPLE_0:def_13; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex a being set ex f being Function st
( [a,f] in the carrier of S \/ the carrier' of S & x in rng f ) ) ) & ( for x being set holds
( x in b2 iff ex a being set ex f being Function st
( [a,f] in the carrier of S \/ the carrier' of S & x in rng f ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means  ex a being set ex 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 S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum
end;
end;

:: deftheorem Def6 defines underlay CATALG_1:def_6_:_
 for S being ManySortedSign
for b2 being set holds
( b2 = underlay S iff for x being set holds
( x in b2 iff ex a being set ex f being Function st
( [a,f] in the carrier of S \/ the carrier' of S & x in rng f ) ) );

theorem Th5: :: CATALG_1:5
for A being set holds underlay (CatSign A) = A
proof
let A be set ; ::_thesis: underlay (CatSign A) = A
set S = CatSign A;
A1: the carrier' of (CatSign A) = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] by Def3;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: A c= underlay (CatSign A)
let x be set ; ::_thesis: ( x in underlay (CatSign A) implies x in A )
assume  x in underlay (CatSign A) ; ::_thesis: x in A
then consider a being set , f being Function such that
A2: [a,f] in the carrier of (CatSign A) \/ the carrier' of (CatSign A) and
A3: x in rng f by Def6;
 ( [a,f] in the carrier of (CatSign A) or [a,f] in the carrier' of (CatSign A) ) 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; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in underlay (CatSign A) )
assume  x in A ; ::_thesis: x in underlay (CatSign A)
then A4: <*x,x*> in 2 -tuples_on A by FINSEQ_2:137;
 the carrier of (CatSign A) = [:{0},(2 -tuples_on A):] by Def3;
then  [0,<*x,x*>] in the carrier of (CatSign A) by A4, ZFMISC_1:105;
then A5: [0,<*x,x*>] in the carrier of (CatSign A) \/ the carrier' of (CatSign A) 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  x in underlay (CatSign A) by A5, Def6; ::_thesis: verum
end;

definition
let S be ManySortedSign ;
attrS is delta-concrete  means :Def7: :: CATALG_1:def 7
 ex f being Function of NAT,NAT st
( ( for s being set st s in the carrier of S holds
ex i being Element of NAT ex 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 holds
ex i being Element of NAT ex p being FinSequence st
( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier' of S ) ) );
end;

:: deftheorem Def7 defines delta-concrete CATALG_1:def_7_:_
 for S being ManySortedSign holds
( S is delta-concrete iff ex f being Function of NAT,NAT st
( ( for s being set st s in the carrier of S holds
ex i being Element of NAT ex 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 holds
ex i being Element of NAT ex p being FinSequence st
( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier' of S ) ) ) );

registration
let A be set ;
cluster CatSign A ->  strict delta-concrete ;
coherence
 CatSign A is delta-concrete
proof
defpred S1[ set , set ] means ( ( A = 0 implies c2 = 2 ) & ( A = 1 implies c2 = 1 ) & ( A = 2 implies c2 = 3 ) );
set S = CatSign A;
A1: for x being set st x in NAT holds
ex y being set st
( y in NAT & S1[x,y] )
proof
reconsider j0 = 2, j1 = 1, j2 = 3 as set ;
let i be set ; ::_thesis: ( i in NAT implies ex y being set st
( y in NAT & S1[i,y] ) )
assume  i in NAT ; ::_thesis: ex y being set st
( y in NAT & S1[i,y] )
percases ( i = 0 or i = 1 or i = 2 or ( i <> 0 & i <> 1 & i <> 2 ) ) ;
supposeA2: i = 0 ; ::_thesis: ex y being set st
( y in NAT & S1[i,y] )
take  j0 ; ::_thesis: ( j0 in NAT & S1[i,j0] )
thus  ( j0 in NAT & S1[i,j0] ) by A2; ::_thesis: verum
end;
supposeA3: i = 1 ; ::_thesis: ex y being set st
( y in NAT & S1[i,y] )
take  j1 ; ::_thesis: ( j1 in NAT & S1[i,j1] )
thus  ( j1 in NAT & S1[i,j1] ) by A3; ::_thesis: verum
end;
supposeA4: i = 2 ; ::_thesis: ex y being set st
( y in NAT & S1[i,y] )
take  j2 ; ::_thesis: ( j2 in NAT & S1[i,j2] )
thus  ( j2 in NAT & S1[i,j2] ) by A4; ::_thesis: verum
end;
supposeA5: ( i <> 0 & i <> 1 & i <> 2 ) ; ::_thesis: ex y being set st
( y in NAT & S1[i,y] )
take  j0 ; ::_thesis: ( j0 in NAT & S1[i,j0] )
thus  ( j0 in NAT & S1[i,j0] ) by A5; ::_thesis: verum
end;
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
S1[i,f . i] from FUNCT_1:sch_5(A1);
reconsider f = f as Function of NAT,NAT by A6, FUNCT_2:2;
take  f ; :: according to CATALG_1:def_7 ::_thesis: ( ( for s being set st s in the carrier of (CatSign A) holds
ex i being Element of NAT ex p being FinSequence st
( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier of (CatSign A) ) ) & ( for o being set st o in the carrier' of (CatSign A) holds
ex i being Element of NAT ex p being FinSequence st
( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) ) ) )
A8: A = underlay (CatSign A) by Th5;
A9: the carrier of (CatSign A) = [:{0},(2 -tuples_on A):] by Def3;
hereby  ::_thesis: for o being set st o in the carrier' of (CatSign A) holds
ex i being Element of NAT ex p being FinSequence st
( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) )
let s be set ; ::_thesis: ( s in the carrier of (CatSign A) implies ex i being Element of NAT ex p being FinSequence st
( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier of (CatSign A) ) )
assume  s in the carrier of (CatSign A) ; ::_thesis: ex i being Element of NAT ex p being FinSequence st
( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier of (CatSign A) )
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 = p as FinSequence by A11;
take i = 0 ; ::_thesis: ex p being FinSequence st
( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier of (CatSign A) )
take p = p; ::_thesis: ( s = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier of (CatSign A) )
 f . i = 2 by A7;
hence  ( s = [i,p] & len p = f . i ) by A10, A11, A12, FINSEQ_2:132, TARSKI:def_1; ::_thesis: [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier of (CatSign A)
thus  [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier of (CatSign A) by A7, A9, A8; ::_thesis: verum
end;
let o be set ; ::_thesis: ( o in the carrier' of (CatSign A) implies ex i being Element of NAT ex p being FinSequence st
( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) ) )
A13: the carrier' of (CatSign A) = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] by Def3;
assume A14: o in the carrier' of (CatSign A) ; ::_thesis: ex i being Element of NAT ex p being FinSequence st
( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) )
percases ( o in [:{1},(1 -tuples_on A):] or o in [:{2},(3 -tuples_on A):] ) by A13, A14, XBOOLE_0:def_3;
suppose o in [:{1},(1 -tuples_on A):] ; ::_thesis: ex i being Element of NAT ex p being FinSequence st
( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign 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 = p as FinSequence of A by A16, FINSEQ_2:def_3;
take i = 1; ::_thesis: ex p being FinSequence st
( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) )
take  p ; ::_thesis: ( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) )
 f . i = 1 by A7;
hence  ( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) ) by A13, A8, A15, A16, A17, FINSEQ_2:132, TARSKI:def_1, XBOOLE_1:7; ::_thesis: verum
end;
suppose o in [:{2},(3 -tuples_on A):] ; ::_thesis: ex i being Element of NAT ex p being FinSequence st
( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign 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 = p as FinSequence of A by A19, FINSEQ_2:def_3;
take i = 2; ::_thesis: ex p being FinSequence st
( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) )
take  p ; ::_thesis: ( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) )
 f . i = 3 by A7;
hence  ( o = [i,p] & len p = f . i & [:{i},((f . i) -tuples_on (underlay (CatSign A))):] c= the carrier' of (CatSign A) ) by A13, A8, A18, A19, A20, FINSEQ_2:132, TARSKI:def_1, XBOOLE_1:7; ::_thesis: verum
end;
end;
end;
end;

registration
cluster non empty strict feasible Categorial delta-concrete for ManySortedSign ;
existence
 ex b1 being CatSignature st
( b1 is delta-concrete & not b1 is empty & b1 is strict )
proof
take  CatSign {{}} ; ::_thesis: ( CatSign {{}} is delta-concrete & not CatSign {{}} is empty & CatSign {{}} is strict )
thus  ( CatSign {{}} is delta-concrete & not CatSign {{}} is empty & CatSign {{}} is strict ) ; ::_thesis: verum
end;
let A be set ;
cluster strict feasible Categorial delta-concrete for CatSignature of A;
existence
 ex b1 being CatSignature of A st
( b1 is delta-concrete & b1 is strict )
proof
take  CatSign A ; ::_thesis: ( CatSign A is delta-concrete & CatSign A is strict )
thus  ( CatSign A is delta-concrete & CatSign A is strict ) ; ::_thesis: verum
end;
end;

theorem Th6: :: CATALG_1:6
for S being delta-concrete ManySortedSign
for x being set st ( x in the carrier of S or x in the carrier' of S ) holds
ex i being Element of NAT ex p being FinSequence st
( x = [i,p] & rng p c= underlay S )
proof
let S be delta-concrete ManySortedSign ; ::_thesis: for x being set st ( x in the carrier of S or x in the carrier' of S ) holds
ex i being Element of NAT ex p being FinSequence st
( x = [i,p] & rng p c= underlay S )
let x be set ; ::_thesis: ( ( x in the carrier of S or x in the carrier' of S ) implies ex i being Element of NAT ex p being FinSequence st
( x = [i,p] & rng p c= underlay S ) )
assume A1: ( x in the carrier of S or x in the carrier' of S ) ; ::_thesis: ex i being Element of NAT ex p being FinSequence st
( x = [i,p] & rng p c= underlay 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 holds
ex i being Element of NAT ex 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 holds
ex i being Element of NAT ex 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;
percases ( x in the carrier of S or x in the carrier' of S ) by A1;
suppose x in the carrier of S ; ::_thesis: ex i being Element of NAT ex p being FinSequence st
( x = [i,p] & rng p c= underlay 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 ; ::_thesis: ex p being FinSequence st
( x = [i,p] & rng p c= underlay S )
take  p ; ::_thesis: ( x = [i,p] & rng p c= underlay S )
thus  x = [i,p] by A5; ::_thesis: rng p c= underlay S
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng p or a in underlay S )
thus  ( not a in rng p or a in underlay S ) by A2, A5, Def6; ::_thesis: verum
end;
suppose x in the carrier' of S ; ::_thesis: ex i being Element of NAT ex p being FinSequence st
( x = [i,p] & rng p c= underlay 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 ; ::_thesis: ex p being FinSequence st
( x = [i,p] & rng p c= underlay S )
take  p ; ::_thesis: ( x = [i,p] & rng p c= underlay S )
thus  x = [i,p] by A6; ::_thesis: rng p c= underlay S
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng p or a in underlay S )
thus  ( not a in rng p or a in underlay S ) by A2, A6, Def6; ::_thesis: verum
end;
end;
end;

theorem :: CATALG_1:7
for S being delta-concrete ManySortedSign
for i being set
for 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 ; ::_thesis: for i being set
for 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
let i be set ; ::_thesis: for 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
let p1, p2 be FinSequence; ::_thesis: ( ( ( [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 ) ) implies len p1 = len p2 )
assume 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 ) ) ; ::_thesis: len p1 = len p2
consider f being Function of NAT,NAT such that
A2: for s being set st s in the carrier of S holds
ex i being Element of NAT ex 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 holds
ex i being Element of NAT ex 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;
percases ( ( [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 ) ) by A1;
supposeA4: ( [i,p1] in the carrier of S & [i,p2] in the carrier of S ) ; ::_thesis: len p1 = len p2
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  len p1 = len p2 by A6, A8, A9, A7, XTUPLE_0:1; ::_thesis: verum
end;
supposeA10: ( [i,p1] in the carrier' of S & [i,p2] in the carrier' of S ) ; ::_thesis: len p1 = len p2
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  len p1 = len p2 by A12, A14, A15, A13, XTUPLE_0:1; ::_thesis: verum
end;
end;
end;

theorem :: CATALG_1:8
for S being delta-concrete ManySortedSign
for i being set
for 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 ; ::_thesis: for i being set
for 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 ) )
let i be set ; ::_thesis: for 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 ) )
let p1, p2 be FinSequence; ::_thesis: ( len p2 = len p1 & rng p2 c= underlay S implies ( ( [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 ) ) )
assume A1: ( len p2 = len p1 & rng p2 c= underlay S ) ; ::_thesis: ( ( [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 ) )
consider f being Function of NAT,NAT such that
A2: for s being set st s in the carrier of S holds
ex i being Element of NAT ex 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 holds
ex i being Element of NAT ex 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  ::_thesis: ( [i,p1] in the carrier' of S implies [i,p2] in the carrier' of S )
assume  [i,p1] in the carrier of S ; ::_thesis: [i,p2] 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; ::_thesis: verum
end;
assume  [i,p1] in the carrier' of S ; ::_thesis: [i,p2] 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  [i,p2] in the carrier' of S by A10; ::_thesis: verum
end;

theorem :: CATALG_1:9
for S being non empty Categorial delta-concrete Signature holds S is CatSignature of underlay S
proof
let S be non empty Categorial delta-concrete Signature; ::_thesis: S is CatSignature of underlay S
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 holds
ex i being Element of NAT ex 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 holds
ex i being Element of NAT ex 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: the SortSymbol of 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 ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in underlay S )
assume  x in A ; ::_thesis: x in underlay S
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  x in underlay S by A8, Def6; ::_thesis: verum
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 ; :: according to TARSKI:def_3 ::_thesis: ( not x in underlay S or x in A )
assume  x in underlay S ; ::_thesis: x in A
then  <*x,x*> in 2 -tuples_on (underlay S) by FINSEQ_2:137;
hence  x in A by A9, FINSEQ_2:138; ::_thesis: verum
end;
then  A = underlay S by A7, XBOOLE_0:def_10;
hence  S is CatSignature of underlay S by A1, A2, Def5; ::_thesis: verum
end;

begin

registration
let S be non empty CatSignature;
let s be SortSymbol of S;
clusters `2  ->  Relation-like Function-like ;
coherence
 ( s `2 is Relation-like & s `2 is Function-like )
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  ( s `2 is Relation-like & s `2 is Function-like ) ; ::_thesis: verum
end;
end;

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

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

registration
let S be non empty CatSignature;
let s be SortSymbol of S;
clusters `2  ->  FinSequence-like ;
coherence
 s `2 is FinSequence-like
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  s `2 is FinSequence-like ; ::_thesis: verum
end;
end;

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

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

definition
let a be set ;
func idsym a ->  set  equals :: CATALG_1:def 8
[1,<*a*>];
correctness
coherence
[1,<*a*>] is set ;
;
let b be set ;
func homsym (a,b) ->  set  equals :: CATALG_1:def 9
[0,<*a,b*>];
correctness
coherence
[0,<*a,b*>] is set ;
;
let c be set ;
func compsym (a,b,c) ->  set  equals :: CATALG_1:def 10
[2,<*a,b,c*>];
correctness
coherence
[2,<*a,b,c*>] is set ;
;
end;

:: deftheorem  defines idsym CATALG_1:def_8_:_
 for a being set holds idsym a = [1,<*a*>];

:: deftheorem  defines homsym CATALG_1:def_9_:_
 for a, b being set holds homsym (a,b) = [0,<*a,b*>];

:: deftheorem  defines compsym CATALG_1:def_10_:_
 for a, b, c being set holds compsym (a,b,c) = [2,<*a,b,c*>];

theorem Th10: :: CATALG_1:10
for A being non empty set
for 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 ; ::_thesis: for 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 ) ) ) )
let S be CatSignature of A; ::_thesis: 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 ) ) ) )
let a be Element of A; ::_thesis: ( 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 ) ) ) )
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; ::_thesis: 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 ) )
let b be Element of A; ::_thesis: ( homsym (a,b) in the carrier of S & ( for c being Element of A holds compsym (a,b,c) in the carrier' of S ) )
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; ::_thesis: for c being Element of A holds compsym (a,b,c) in the carrier' of S
let c be Element of A; ::_thesis: compsym (a,b,c) in the carrier' of S
 <*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  compsym (a,b,c) in the carrier' of S by A4; ::_thesis: verum
end;

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

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

theorem Th12: :: CATALG_1:12
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 ; ::_thesis: ( homsym (a1,a2) = homsym (b1,b2) implies ( a1 = b1 & a2 = b2 ) )
assume  homsym (a1,a2) = homsym (b1,b2) ; ::_thesis: ( a1 = b1 & a2 = b2 )
then A1: <*a1,a2*> = <*b1,b2*> by XTUPLE_0:1;
 ( <*a1,a2*> . 1 = a1 & <*a1,a2*> . 2 = a2 ) by FINSEQ_1:44;
hence  ( a1 = b1 & a2 = b2 ) by A1, FINSEQ_1:44; ::_thesis: verum
end;

theorem Th13: :: CATALG_1:13
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 ; ::_thesis: ( compsym (a1,a2,a3) = compsym (b1,b2,b3) implies ( a1 = b1 & a2 = b2 & a3 = b3 ) )
A1: <*a1,a2,a3*> . 3 = a3 by FINSEQ_1:45;
assume  compsym (a1,a2,a3) = compsym (b1,b2,b3) ; ::_thesis: ( a1 = b1 & a2 = b2 & a3 = 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  ( a1 = b1 & a2 = b2 & a3 = b3 ) by A2, A1, FINSEQ_1:45; ::_thesis: verum
end;

theorem Th14: :: CATALG_1:14
for A being non empty set
for 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 ; ::_thesis: for S being CatSignature of A
for s being SortSymbol of S ex a, b being Element of A st s = homsym (a,b)
let S be CatSignature of A; ::_thesis: for s being SortSymbol of S ex a, b being Element of A st s = homsym (a,b)
let s be SortSymbol of S; ::_thesis: ex a, b being Element of A st s = homsym (a,b)
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 ; ::_thesis: ex b being Element of A st s = homsym (a,b)
take  b ; ::_thesis: s = homsym (a,b)
 ( s = [(s `1),(s `2)] & s `1 in {0} ) by A1, MCART_1:10, MCART_1:21;
hence  s = homsym (a,b) by A2, A5, TARSKI:def_1; ::_thesis: verum
end;

theorem Th15: :: CATALG_1:15
for A being non empty set
for 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 ; ::_thesis: for o being OperSymbol of (CatSign A) holds
( ( o `1 = 1 & len (o `2) = 1 ) or ( o `1 = 2 & len (o `2) = 3 ) )
let o be OperSymbol of (CatSign A); ::_thesis: ( ( o `1 = 1 & len (o `2) = 1 ) or ( o `1 = 2 & 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  ( ( 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  ( ( o `1 = 1 & len (o `2) = 1 ) or ( o `1 = 2 & len (o `2) = 3 ) ) by CARD_1:def_7, TARSKI:def_1; ::_thesis: verum
end;

theorem Th16: :: CATALG_1:16
for A being non empty set
for o being OperSymbol of (CatSign A) st ( o `1 = 1 or len (o `2) = 1 ) holds
ex a being Element of A st o = idsym a
proof
let A be non empty set ; ::_thesis: for o being OperSymbol of (CatSign A) st ( o `1 = 1 or len (o `2) = 1 ) holds
ex a being Element of A st o = idsym a
let o be OperSymbol of (CatSign A); ::_thesis: ( ( o `1 = 1 or len (o `2) = 1 ) implies ex a being Element of A st o = idsym a )
assume A1: ( o `1 = 1 or len (o `2) = 1 ) ; ::_thesis: ex a being Element of A st o = idsym 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 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, MCART_1: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 = a as Element of A by A3;
take  a ; ::_thesis: o = idsym a
thus  o = idsym a by A1, A2, A4, CARD_1:def_7, TARSKI:def_1; ::_thesis: verum
end;

theorem Th17: :: CATALG_1:17
for A being non empty set
for o being OperSymbol of (CatSign A) st ( o `1 = 2 or len (o `2) = 3 ) holds
ex a, b, c being Element of A st o = compsym (a,b,c)
proof
let A be non empty set ; ::_thesis: for o being OperSymbol of (CatSign A) st ( o `1 = 2 or len (o `2) = 3 ) holds
ex a, b, c being Element of A st o = compsym (a,b,c)
let o be OperSymbol of (CatSign A); ::_thesis: ( ( o `1 = 2 or len (o `2) = 3 ) implies ex a, b, c being Element of A st o = compsym (a,b,c) )
assume A1: ( o `1 = 2 or len (o `2) = 3 ) ; ::_thesis: ex a, b, c being Element of A st o = compsym (a,b,c)
 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, MCART_1: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 = a, b = b, c = c as Element of A by A3;
take  a ; ::_thesis: ex b, c being Element of A st o = compsym (a,b,c)
take  b ; ::_thesis: ex c being Element of A st o = compsym (a,b,c)
take  c ; ::_thesis: o = compsym (a,b,c)
thus  o = compsym (a,b,c) by A1, A2, A4, CARD_1:def_7, TARSKI:def_1; ::_thesis: verum
end;

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

theorem :: CATALG_1:19
for A being non empty set
for 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

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: :: CATALG_1:def 11
 for s being SortSymbol of (CatSign the carrier of C1) holds it . s = [0,((Obj F) * (s `2))];
uniqueness
 for b1, b2 being Function of the carrier of (CatSign the carrier of C1), the carrier of (CatSign the carrier of C2) st ( for s being SortSymbol of (CatSign the carrier of C1) holds b1 . s = [0,((Obj F) * (s `2))] ) & ( for s being SortSymbol of (CatSign the carrier of C1) holds b2 . s = [0,((Obj F) * (s `2))] ) holds
b1 = b2
proof
let U1, U2 be Function of the carrier of (CatSign the carrier of C1), the carrier of (CatSign the carrier of C2); ::_thesis: ( ( for s being SortSymbol of (CatSign the carrier of C1) holds U1 . s = [0,((Obj F) * (s `2))] ) & ( for s being SortSymbol of (CatSign the carrier of C1) holds U2 . s = [0,((Obj F) * (s `2))] ) implies U1 = U2 )
assume 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))] ; ::_thesis: U1 = U2
now__::_thesis:_for_s_being_SortSymbol_of_(CatSign_the_carrier_of_C1)_holds_U1_._s_=_U2_._s
let s be SortSymbol of (CatSign the carrier of C1); ::_thesis: U1 . s = U2 . s
thus U1 . s = [0,((Obj F) * (s `2))] by A1
.= U2 . s by A2 ; ::_thesis: verum
end;
hence  U1 = U2 by FUNCT_2:63; ::_thesis: verum
end;
existence
 ex b1 being Function of the carrier of (CatSign the carrier of C1), the carrier of (CatSign the carrier of C2) st
for s being SortSymbol of (CatSign the carrier of C1) holds b1 . s = [0,((Obj F) * (s `2))]
proof
deffunc H1( SortSymbol of (CatSign the carrier of C1)) ->  set = [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 = H1(s) from FUNCT_1:sch_4();
 rng Up c= the carrier of (CatSign the carrier of C2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng Up or x in the carrier of (CatSign the carrier of C2) )
assume  x in rng Up ; ::_thesis: x in the carrier of (CatSign the carrier of C2)
then consider a being set  such that
A5: a in dom Up and
A6: x = Up . a by FUNCT_1:def_3;
reconsider a = 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 = a1, a2 = 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  x in the carrier of (CatSign the carrier of C2) by A4, A6, A8; ::_thesis: verum
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  ex b1 being Function of the carrier of (CatSign the carrier of C1), the carrier of (CatSign the carrier of C2) st
for s being SortSymbol of (CatSign the carrier of C1) holds b1 . s = [0,((Obj F) * (s `2))] by A4; ::_thesis: verum
end;
func Psi F ->  Function of the carrier' of (CatSign the carrier of C1), the carrier' of (CatSign the carrier of C2) means :Def12: :: CATALG_1:def 12
 for o being OperSymbol of (CatSign the carrier of C1) holds it . o = [(o `1),((Obj F) * (o `2))];
uniqueness
 for b1, b2 being Function of the carrier' of (CatSign the carrier of C1), the carrier' of (CatSign the carrier of C2) st ( for o being OperSymbol of (CatSign the carrier of C1) holds b1 . o = [(o `1),((Obj F) * (o `2))] ) & ( for o being OperSymbol of (CatSign the carrier of C1) holds b2 . o = [(o `1),((Obj F) * (o `2))] ) holds
b1 = b2
proof
let U1, U2 be Function of the carrier' of (CatSign the carrier of C1), the carrier' of (CatSign the carrier of C2); ::_thesis: ( ( for o being OperSymbol of (CatSign the carrier of C1) holds U1 . o = [(o `1),((Obj F) * (o `2))] ) & ( for o being OperSymbol of (CatSign the carrier of C1) holds U2 . o = [(o `1),((Obj F) * (o `2))] ) implies U1 = U2 )
assume 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))] ; ::_thesis: U1 = U2
now__::_thesis:_for_s_being_OperSymbol_of_(CatSign_the_carrier_of_C1)_holds_U1_._s_=_U2_._s
let s be OperSymbol of (CatSign the carrier of C1); ::_thesis: U1 . s = U2 . s
thus U1 . s = [(s `1),((Obj F) * (s `2))] by A13
.= U2 . s by A14 ; ::_thesis: verum
end;
hence  U1 = U2 by FUNCT_2:63; ::_thesis: verum
end;
existence
 ex b1 being Function of the carrier' of (CatSign the carrier of C1), the carrier' of (CatSign the carrier of C2) st
for o being OperSymbol of (CatSign the carrier of C1) holds b1 . o = [(o `1),((Obj F) * (o `2))]
proof
deffunc H1( OperSymbol of (CatSign the carrier of C1)) ->  set = [($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 = H1(s) from FUNCT_1:sch_4();
 rng Up c= the carrier' of (CatSign the carrier of C2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng Up or x in the carrier' of (CatSign the carrier of C2) )
assume  x in rng Up ; ::_thesis: x in the carrier' of (CatSign the carrier of C2)
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 = a as OperSymbol of (CatSign the carrier of C1) by A15, A17;
percases ( a in [:{1},(1 -tuples_on the carrier of C1):] or a in [:{2},(3 -tuples_on the carrier of C1):] ) by A19, XBOOLE_0:def_3;
supposeA20: a in [:{1},(1 -tuples_on the carrier of C1):] ; ::_thesis: x in the carrier' of (CatSign the carrier of C2)
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 = 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  x in the carrier' of (CatSign the carrier of C2) by A16, A18, A26, A22; ::_thesis: verum
end;
supposeA27: a in [:{2},(3 -tuples_on the carrier of C1):] ; ::_thesis: x in the carrier' of (CatSign the carrier of C2)
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 = a1, a2 = a2, a3 = 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  x in the carrier' of (CatSign the carrier of C2) by A16, A18, A35, A29; ::_thesis: verum
end;
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  ex b1 being Function of the carrier' of (CatSign the carrier of C1), the carrier' of (CatSign the carrier of C2) st
for o being OperSymbol of (CatSign the carrier of C1) holds b1 . o = [(o `1),((Obj F) * (o `2))] by A16; ::_thesis: verum
end;
end;

:: deftheorem Def11 defines Upsilon CATALG_1:def_11_:_
 for C1, C2 being Category
for F being Functor of C1,C2
for b4 being Function of the carrier of (CatSign the carrier of C1), the carrier of (CatSign the carrier of C2) holds
( b4 = Upsilon F iff for s being SortSymbol of (CatSign the carrier of C1) holds b4 . s = [0,((Obj F) * (s `2))] );

:: deftheorem Def12 defines Psi CATALG_1:def_12_:_
 for C1, C2 being Category
for F being Functor of C1,C2
for b4 being Function of the carrier' of (CatSign the carrier of C1), the carrier' of (CatSign the carrier of C2) holds
( b4 = Psi F iff for o being OperSymbol of (CatSign the carrier of C1) holds b4 . o = [(o `1),((Obj F) * (o `2))] );

Lm2: now__::_thesis:_for_x_being_set_
for_f_being_Function_st_x_in_dom_f_holds_
f_*_<*x*>_=_<*(f_._x)*>
let x be set ; ::_thesis: for f being Function st x in dom f holds
f * <*x*> = <*(f . x)*>
let f be Function; ::_thesis: ( x in dom f implies f * <*x*> = <*(f . x)*> )
assume  x in dom f ; ::_thesis: f * <*x*> = <*(f . x)*>
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; ::_thesis: verum
end;

theorem Th20: :: CATALG_1:20
for C1, C2 being Category
for 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; ::_thesis: for F being Functor of C1,C2
for a, b being Object of C1 holds (Upsilon F) . (homsym (a,b)) = homsym ((F . a),(F . b))
let F be Functor of C1,C2; ::_thesis: for a, b being Object of C1 holds (Upsilon F) . (homsym (a,b)) = homsym ((F . a),(F . b))
let a, b be Object of C1; ::_thesis: (Upsilon F) . (homsym (a,b)) = homsym ((F . a),(F . b))
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)) ; ::_thesis: verum
end;

theorem Th21: :: CATALG_1:21
for C1, C2 being Category
for 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; ::_thesis: for F being Functor of C1,C2
for a being Object of C1 holds (Psi F) . (idsym a) = idsym (F . a)
let F be Functor of C1,C2; ::_thesis: for a being Object of C1 holds (Psi F) . (idsym a) = idsym (F . a)
let a be Object of C1; ::_thesis: (Psi F) . (idsym a) = idsym (F . a)
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) ;
::_thesis: verum
end;

theorem Th22: :: CATALG_1:22
for C1, C2 being Category
for 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; ::_thesis: for 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))
let F be Functor of C1,C2; ::_thesis: for a, b, c being Object of C1 holds (Psi F) . (compsym (a,b,c)) = compsym ((F . a),(F . b),(F . c))
let a, b, c be Object of C1; ::_thesis: (Psi F) . (compsym (a,b,c)) = compsym ((F . a),(F . b),(F . c))
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)) ;
::_thesis: verum
end;

theorem Th23: :: CATALG_1:23
for C1, C2 being Category
for 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; ::_thesis: for F being Functor of C1,C2 holds Upsilon F, Psi F form_morphism_between CatSign the carrier of C1, CatSign the carrier of C2
let F be Functor of C1,C2; ::_thesis: Upsilon F, Psi F form_morphism_between CatSign the carrier of C1, CatSign the carrier of C2
set f = Upsilon F;
set g = Psi F;
set S1 = CatSign the carrier of C1;
set S2 = CatSign the carrier of C2;
thus  ( dom (Upsilon F) = the carrier of (CatSign the carrier of C1) & dom (Psi F) = the carrier' of (CatSign the carrier of C1) ) by FUNCT_2:def_1; :: according to PUA2MSS1:def_12 ::_thesis: ( proj2 (Upsilon F) c= the carrier of (CatSign the carrier of C2) & proj2 (Psi F) c= the carrier' of (CatSign the carrier of C2) & the ResultSort of (CatSign the carrier of C1) * (Upsilon F) = (Psi F) * the ResultSort of (CatSign the carrier of C2) & ( for b1 being set
for b2 being set holds
( not b1 in the carrier' of (CatSign the carrier of C1) or not b2 = the Arity of (CatSign the carrier of C1) . b1 or b2 * (Upsilon F) = the Arity of (CatSign the carrier of C2) . ((Psi F) . b1) ) ) )
thus  ( rng (Upsilon F) c= the carrier of (CatSign the carrier of C2) & rng (Psi F) c= the carrier' of (CatSign the carrier of C2) ) ; ::_thesis: ( the ResultSort of (CatSign the carrier of C1) * (Upsilon F) = (Psi F) * the ResultSort of (CatSign the carrier of C2) & ( for b1 being set
for b2 being set holds
( not b1 in the carrier' of (CatSign the carrier of C1) or not b2 = the Arity of (CatSign the carrier of C1) . b1 or b2 * (Upsilon F) = the Arity of (CatSign the carrier of C2) . ((Psi F) . b1) ) ) )
now__::_thesis:_for_o_being_OperSymbol_of_(CatSign_the_carrier_of_C1)_holds_((Upsilon_F)_*_the_ResultSort_of_(CatSign_the_carrier_of_C1))_._o_=_(_the_ResultSort_of_(CatSign_the_carrier_of_C2)_*_(Psi_F))_._o
let o be OperSymbol of (CatSign the carrier of C1); ::_thesis: ((Upsilon F) * the ResultSort of (CatSign the carrier of C1)) . b1 = ( the ResultSort of (CatSign the carrier of C2) * (Psi F)) . b1
percases ( o `1 = 1 or o `1 = 2 ) by Th15;
suppose o `1 = 1 ; ::_thesis: ((Upsilon F) * the ResultSort of (CatSign the carrier of C1)) . b1 = ( the ResultSort of (CatSign the carrier of C2) * (Psi F)) . b1
then consider a being Object of C1 such that
A1: o = idsym a by Th16;
thus ((Upsilon F) * the ResultSort of (CatSign the carrier of C1)) . o = (Upsilon F) . (the_result_sort_of o) by FUNCT_2:15
.= (Upsilon 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 (CatSign the carrier of C2) . ((Psi F) . (idsym a)) by Th21
.= ( the ResultSort of (CatSign the carrier of C2) * (Psi F)) . o by A1, FUNCT_2:15 ; ::_thesis: verum
end;
suppose o `1 = 2 ; ::_thesis: ((Upsilon F) * the ResultSort of (CatSign the carrier of C1)) . b1 = ( the ResultSort of (CatSign the carrier of C2) * (Psi F)) . b1
then consider a, b, c being Object of C1 such that
A2: o = compsym (a,b,c) by Th17;
thus ((Upsilon F) * the ResultSort of (CatSign the carrier of C1)) . o = (Upsilon F) . (the_result_sort_of o) by FUNCT_2:15
.= (Upsilon 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 (CatSign the carrier of C2) . ((Psi F) . (compsym (a,b,c))) by Th22
.= ( the ResultSort of (CatSign the carrier of C2) * (Psi F)) . o by A2, FUNCT_2:15 ; ::_thesis: verum
end;
end;
end;
hence  (Upsilon F) * the ResultSort of (CatSign the carrier of C1) = the ResultSort of (CatSign the carrier of C2) * (Psi F) by FUNCT_2:63; ::_thesis: for b1 being set
for b2 being set holds
( not b1 in the carrier' of (CatSign the carrier of C1) or not b2 = the Arity of (CatSign the carrier of C1) . b1 or b2 * (Upsilon F) = the Arity of (CatSign the carrier of C2) . ((Psi F) . b1) )
let o be set ; ::_thesis: for b1 being set holds
( not o in the carrier' of (CatSign the carrier of C1) or not b1 = the Arity of (CatSign the carrier of C1) . o or b1 * (Upsilon F) = the Arity of (CatSign the carrier of C2) . ((Psi F) . o) )
let p be Function; ::_thesis: ( not o in the carrier' of (CatSign the carrier of C1) or not p = the Arity of (CatSign the carrier of C1) . o or p * (Upsilon F) = the Arity of (CatSign the carrier of C2) . ((Psi F) . o) )
assume  o in the carrier' of (CatSign the carrier of C1) ; ::_thesis: ( not p = the Arity of (CatSign the carrier of C1) . o or p * (Upsilon F) = the Arity of (CatSign the carrier of C2) . ((Psi F) . o) )
then reconsider o9 = o as OperSymbol of (CatSign the carrier of C1) ;
assume A3: p = the Arity of (CatSign the carrier of C1) . o ; ::_thesis: p * (Upsilon F) = the Arity of (CatSign the carrier of C2) . ((Psi F) . o)
percases ( o9 `1 = 1 or o9 `1 = 2 ) by Th15;
suppose o9 `1 = 1 ; ::_thesis: p * (Upsilon F) = the Arity of (CatSign the carrier of C2) . ((Psi F) . o)
then consider a being Object of C1 such that
A4: o = idsym a by Th16;
A5: (Upsilon F) * {} = {} ;
 p = {} by A3, A4, Def3;
hence (Upsilon F) * p = the_arity_of (idsym (F . a)) by A5, Def3
.= the Arity of (CatSign the carrier of C2) . ((Psi F) . o) by A4, Th21 ;
::_thesis: verum
end;
suppose o9 `1 = 2 ; ::_thesis: p * (Upsilon F) = the Arity of (CatSign the carrier of C2) . ((Psi F) . o)
then consider a, b, c being Object of C1 such that
A6: o = compsym (a,b,c) by Th17;
 ( dom (Upsilon F) = the carrier of (CatSign the carrier of C1) & p = <*(homsym (b,c)),(homsym (a,b))*> ) by A3, A6, Def3, FUNCT_2:def_1;
hence (Upsilon F) * p = <*((Upsilon F) . (homsym (b,c))),((Upsilon F) . (homsym (a,b)))*> by FINSEQ_2:125
.= <*(homsym ((F . b),(F . c))),((Upsilon 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 (CatSign the carrier of C2) . ((Psi F) . o) by A6, Th22 ;
::_thesis: verum
end;
end;
end;

begin

theorem Th24: :: CATALG_1:24
for C being non empty set
for A being MSAlgebra over CatSign C
for a being Element of C holds Args ((idsym a),A) = {{}}
proof
let C be non empty set ; ::_thesis: for A being MSAlgebra over CatSign C
for a being Element of C holds Args ((idsym a),A) = {{}}
let A be MSAlgebra over CatSign C; ::_thesis: for a being Element of C holds Args ((idsym a),A) = {{}}
let a be Element of C; ::_thesis: Args ((idsym a),A) = {{}}
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 ; ::_thesis: verum
end;

Lm3:  for C being Category
for 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) ) holds
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; ::_thesis: for 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) ) holds
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) )
let A be MSAlgebra over CatSign the carrier of C; ::_thesis: ( ( for a, b being Object of C holds the Sorts of A . (homsym (a,b)) = Hom (a,b) ) implies 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) ) )
assume A1: for a, b being Object of C holds the Sorts of A . (homsym (a,b)) = Hom (a,b) ; ::_thesis: 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) )
let a, b, c be Object of C; ::_thesis: ( Args ((compsym (a,b,c)),A) = product <*(Hom (b,c)),(Hom (a,b))*> & Result ((compsym (a,b,c)),A) = Hom (a,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 ; ::_thesis: Result ((compsym (a,b,c)),A) = Hom (a,c)
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 ; ::_thesis: verum
end;

scheme :: CATALG_1:sch 1
CatAlgEx{ F1() ->  non empty set , F2() ->  non empty set , F3( set , set ) ->  set , F4( set , set , set , set , set ) ->  set , F5( set ) ->  set } :
 ex A being strict MSAlgebra over CatSign F1() st
( ( for a, b being Element of F1() holds the Sorts of A . (homsym (a,b)) = F3(a,b) ) & ( for a being Element of F1() holds (Den ((idsym a),A)) . {} = F5(a) ) & ( for a, b, c being Element of F1()
for f, g being Element of F2() st f in F3(a,b) & g in F3(b,c) holds
(Den ((compsym (a,b,c)),A)) . <*g,f*> = F4(a,b,c,g,f) ) )
provided
A1: for a, b being Element of F1() holds F3(a,b) c= F2() and
A2: for a being Element of F1() holds F5(a) in F3(a,a) and
A3: for a, b, c being Element of F1()
for f, g being Element of F2() st f in F3(a,b) & g in F3(b,c) holds
F4(a,b,c,g,f) in F3(a,c)
proof
defpred S1[ set , set ] means ( ( $1 `1 = 1 & ex a being Element of F1() st
( $1 = idsym a & ex F being Function of {{}},F3(a,a) st
( F = $2 & F . {} = F5(a) ) ) ) or ( $1 `1 = 2 & ex a, b, c being Element of F1() st
( $1 = compsym (a,b,c) & ex F being Function of (product <*F3(b,c),F3(a,b)*>),F3(a,c) st
( F = $2 & ( for f, g being set st f in F3(a,b) & g in F3(b,c) holds
F . <*g,f*> = F4(a,b,c,g,f) ) ) ) ) );
set CS = CatSign F1();
A4: for o being set st o in the carrier' of (CatSign F1()) holds
ex u being set st S1[o,u]
proof
let o be set ; ::_thesis: ( o in the carrier' of (CatSign F1()) implies ex u being set st S1[o,u] )
assume A5: o in the carrier' of (CatSign F1()) ; ::_thesis: ex u being set st S1[o,u]
A6: now__::_thesis:_(_o_`1_=_1_implies_ex_u_being_set_ex_a_being_Element_of_F1()_st_
(_o_=_idsym_a_&_ex_F_being_Function_of_{{}},F3(a,a)_st_
(_F_=_u_&_F_._{}_=_F5(a)_)_)_)
assume  o `1 = 1 ; ::_thesis: ex u being set ex a being Element of F1() st
( o = idsym a & ex F being Function of {{}},F3(a,a) st
( F = u & F . {} = F5(a) ) )
then consider a being Element of F1() such that
A7: o = idsym a by A5, Th16;
set F = {} :-> F5(a);
reconsider u = {} :-> F5(a) as set ;
take u = u; ::_thesis: ex a being Element of F1() st
( o = idsym a & ex F being Function of {{}},F3(a,a) st
( F = u & F . {} = F5(a) ) )
take a = a; ::_thesis: ( o = idsym a & ex F being Function of {{}},F3(a,a) st
( F = u & F . {} = F5(a) ) )
thus  o = idsym a by A7; ::_thesis: ex F being Function of {{}},F3(a,a) st
( F = u & F . {} = F5(a) )
 F5(a) in F3(a,a) by A2;
then  {F5(a)} c= F3(a,a) by ZFMISC_1:31;
then  ( dom ({} :-> F5(a)) = {{}} & rng ({} :-> F5(a)) c= F3(a,a) ) by FUNCOP_1:13, XBOOLE_1:1;
then reconsider F = {} :-> F5(a) as Function of {{}},F3(a,a) by FUNCT_2:2;
take F = F; ::_thesis: ( F = u & F . {} = F5(a) )
 {} in {{}} by TARSKI:def_1;
hence  ( F = u & F . {} = F5(a) ) by FUNCOP_1:7; ::_thesis: verum
end;
A8: now__::_thesis:_(_o_`1_=_2_implies_ex_u_being_set_ex_a,_b,_c_being_Element_of_F1()_st_
(_o_=_compsym_(a,b,c)_&_ex_F_being_Function_of_(product_<*F3(b,c),F3(a,b)*>),F3(a,c)_st_
(_F_=_u_&_(_for_f,_g_being_set_st_f_in_F3(a,b)_&_g_in_F3(b,c)_holds_
F_._<*g,f*>_=_F4(a,b,c,g,f)_)_)_)_)
assume  o `1 = 2 ; ::_thesis: ex u being set ex a, b, c being Element of F1() st
( o = compsym (a,b,c) & ex F being Function of (product <*F3(b,c),F3(a,b)*>),F3(a,c) st
( F = u & ( for f, g being set st f in F3(a,b) & g in F3(b,c) holds
F . <*g,f*> = F4(a,b,c,g,f) ) ) )
then consider a, b, c being Element of F1() such that
A9: o = compsym (a,b,c) by A5, Th17;
defpred S2[ set , set ] means  ex f, g being set st
( f in F3(a,b) & g in F3(b,c) & $1 = <*g,f*> & $2 = F4(a,b,c,g,f) );
A10: now__::_thesis:_for_x_being_set_st_x_in_product_<*F3(b,c),F3(a,b)*>_holds_
ex_u_being_set_st_
(_u_in_F3(a,c)_&_S2[x,u]_)
let x be set ; ::_thesis: ( x in product <*F3(b,c),F3(a,b)*> implies ex u being set st
( u in F3(a,c) & S2[x,u] ) )
assume  x in product <*F3(b,c),F3(a,b)*> ; ::_thesis: ex u being set st
( u in F3(a,c) & S2[x,u] )
then consider g, f being set  such that
A11: ( g in F3(b,c) & f in F3(a,b) ) and
A12: x = <*g,f*> by FINSEQ_3:124;
take u = F4(a,b,c,g,f); ::_thesis: ( u in F3(a,c) & S2[x,u] )
 ( F3(a,b) c= F2() & F3(b,c) c= F2() ) by A1;
hence  u in F3(a,c) by A3, A11; ::_thesis: S2[x,u]
thus  S2[x,u] by A11, A12; ::_thesis: verum
end;
consider F being Function such that
A13: ( dom F = product <*F3(b,c),F3(a,b)*> & rng F c= F3(a,c) ) and
A14: for x being set st x in product <*F3(b,c),F3(a,b)*> holds
S2[x,F . x] from FUNCT_1:sch_5(A10);
reconsider u = F as set ;
take u = u; ::_thesis: ex a, b, c being Element of F1() st
( o = compsym (a,b,c) & ex F being Function of (product <*F3(b,c),F3(a,b)*>),F3(a,c) st
( F = u & ( for f, g being set st f in F3(a,b) & g in F3(b,c) holds
F . <*g,f*> = F4(a,b,c,g,f) ) ) )
take a = a; ::_thesis: ex b, c being Element of F1() st
( o = compsym (a,b,c) & ex F being Function of (product <*F3(b,c),F3(a,b)*>),F3(a,c) st
( F = u & ( for f, g being set st f in F3(a,b) & g in F3(b,c) holds
F . <*g,f*> = F4(a,b,c,g,f) ) ) )
take b = b; ::_thesis: ex c being Element of F1() st
( o = compsym (a,b,c) & ex F being Function of (product <*F3(b,c),F3(a,b)*>),F3(a,c) st
( F = u & ( for f, g being set st f in F3(a,b) & g in F3(b,c) holds
F . <*g,f*> = F4(a,b,c,g,f) ) ) )
take c = c; ::_thesis: ( o = compsym (a,b,c) & ex F being Function of (product <*F3(b,c),F3(a,b)*>),F3(a,c) st
( F = u & ( for f, g being set st f in F3(a,b) & g in F3(b,c) holds
F . <*g,f*> = F4(a,b,c,g,f) ) ) )
thus  o = compsym (a,b,c) by A9; ::_thesis: ex F being Function of (product <*F3(b,c),F3(a,b)*>),F3(a,c) st
( F = u & ( for f, g being set st f in F3(a,b) & g in F3(b,c) holds
F . <*g,f*> = F4(a,b,c,g,f) ) )
reconsider F = F as Function of (product <*F3(b,c),F3(a,b)*>),F3(a,c) by A13, FUNCT_2:2;
take F = F; ::_thesis: ( F = u & ( for f, g being set st f in F3(a,b) & g in F3(b,c) holds
F . <*g,f*> = F4(a,b,c,g,f) ) )
thus  F = u ; ::_thesis: for f, g being set st f in F3(a,b) & g in F3(b,c) holds
F . <*g,f*> = F4(a,b,c,g,f)
let f, g be set ; ::_thesis: ( f in F3(a,b) & g in F3(b,c) implies F . <*g,f*> = F4(a,b,c,g,f) )
assume  ( f in F3(a,b) & g in F3(b,c) ) ; ::_thesis: F . <*g,f*> = F4(a,b,c,g,f)
then  <*g,f*> in product <*F3(b,c),F3(a,b)*> by FINSEQ_3:124;
then consider f9, g9 being set  such that
 f9 in F3(a,b) and
 g9 in F3(b,c) and
A15: <*g,f*> = <*g9,f9*> and
A16: F . <*g,f*> = F4(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*> = F4(a,b,c,g,f) by A15, A16, A17, FINSEQ_1:44; ::_thesis: verum
end;
 ( o `1 = 1 or o `1 = 2 ) by A5, Th15;
hence  ex u being set st S1[o,u] by A6, A8; ::_thesis: verum
end;
consider O being Function such that
A18: dom O = the carrier' of (CatSign F1()) and
A19: for o being set st o in the carrier' of (CatSign F1()) holds
S1[o,O . o] from CLASSES1:sch_1(A4);
reconsider O = O as ManySortedSet of the carrier' of (CatSign F1()) by A18, PARTFUN1:def_2, RELAT_1:def_18;
defpred S2[ set , set ] means  ex a, b being Element of F1() st
( $1 = homsym (a,b) & $2 = F3(a,b) );
A20: now__::_thesis:_for_s_being_set_st_s_in_the_carrier_of_(CatSign_F1())_holds_
ex_u_being_set_st_S2[s,u]
let s be set ; ::_thesis: ( s in the carrier of (CatSign F1()) implies ex u being set st S2[s,u] )
assume  s in the carrier of (CatSign F1()) ; ::_thesis: ex u being set st S2[s,u]
then consider a, b being Element of F1() such that
A21: s = homsym (a,b) by Th14;
take u = F3(a,b); ::_thesis: S2[s,u]
thus  S2[s,u] by A21; ::_thesis: verum
end;
consider S being Function such that
A22: dom S = the carrier of (CatSign F1()) and
A23: for s being set st s in the carrier of (CatSign F1()) holds
S2[s,S . s] from CLASSES1:sch_1(A20);
reconsider S = S as ManySortedSet of the carrier of (CatSign F1()) by A22, PARTFUN1:def_2, RELAT_1:def_18;
 O is ManySortedFunction of (S #) * the Arity of (CatSign F1()),S * the ResultSort of (CatSign F1())
proof
let o be set ; :: according to PBOOLE:def_15 ::_thesis: ( not o in the carrier' of (CatSign F1()) or O . o is Element of bool [:(((S #) * the Arity of (CatSign F1())) . o),((S * the ResultSort of (CatSign F1())) . o):] )
assume  o in the carrier' of (CatSign F1()) ; ::_thesis: O . o is Element of bool [:(((S #) * the Arity of (CatSign F1())) . o),((S * the ResultSort of (CatSign F1())) . o):]
then reconsider o = o as OperSymbol of (CatSign F1()) ;
A24: ((S #) * the Arity of (CatSign F1())) . 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 (CatSign F1())) . o = S . (the_result_sort_of o) by FUNCT_2:15;
percases ( ( o `1 = 1 & 1 <> 2 ) or ( o `1 = 2 & 1 <> 2 ) ) by Th15;
suppose ( o `1 = 1 & 1 <> 2 ) ; ::_thesis: O . o is Element of bool [:(((S #) * the Arity of (CatSign F1())) . o),((S * the ResultSort of (CatSign F1())) . o):]
then consider a being Element of F1() such that
A26: ( o = idsym a & ex F being Function of {{}},F3(a,a) st
( F = O . o & F . {} = F5(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 F1() such that
A29: homsym (a,a) = homsym (c,b) and
A30: S . (homsym (a,a)) = F3(c,b) by A23;
 ( a = b & a = c ) by A29, Th12;
hence  O . o is Element of bool [:(((S #) * the Arity of (CatSign F1())) . o),((S * the ResultSort of (CatSign F1())) . o):] by A24, A25, A26, A30, A27, A28, CARD_3:10; ::_thesis: verum
end;
suppose ( o `1 = 2 & 1 <> 2 ) ; ::_thesis: O . o is Element of bool [:(((S #) * the Arity of (CatSign F1())) . o),((S * the ResultSort of (CatSign F1())) . o):]
then consider a, b, c being Element of F1() such that
A31: o = compsym (a,b,c) and
A32: ex F being Function of (product <*F3(b,c),F3(a,b)*>),F3(a,c) st
( F = O . o & ( for f, g being set st f in F3(a,b) & g in F3(b,c) holds
F . <*g,f*> = F4(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 F1() such that
A34: homsym (a,c) = homsym (ax,cx) and
A35: S . (homsym (a,c)) = F3(ax,cx) by A23;
 ( ax = a & cx = c ) by A34, Th12;
then A36: (S * the ResultSort of (CatSign F1())) . o = F3(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 F1() such that
A38: homsym (a,b) = homsym (a9,b9) and
A39: S . (homsym (a,b)) = F3(a9,b9) by A23;
consider b99, c9 being Element of F1() such that
A40: homsym (b,c) = homsym (b99,c9) and
A41: S . (homsym (b,c)) = F3(b99,c9) by A23;
A42: ( b99 = b & c9 = c ) by A40, Th12;
 ( a9 = a & b9 = b ) by A38, Th12;
then  ((S #) * the Arity of (CatSign F1())) . o = product <*F3(b,c),F3(a,b)*> by A22, A24, A31, A39, A41, A42, A37, FINSEQ_2:125;
hence  O . o is Element of bool [:(((S #) * the Arity of (CatSign F1())) . o),((S * the ResultSort of (CatSign F1())) . o):] by A32, A36; ::_thesis: verum
end;
end;
end;
then reconsider O = O as ManySortedFunction of (S #) * the Arity of (CatSign F1()),S * the ResultSort of (CatSign F1()) ;
take A = MSAlgebra(# S,O #); ::_thesis: ( ( for a, b being Element of F1() holds the Sorts of A . (homsym (a,b)) = F3(a,b) ) & ( for a being Element of F1() holds (Den ((idsym a),A)) . {} = F5(a) ) & ( for a, b, c being Element of F1()
for f, g being Element of F2() st f in F3(a,b) & g in F3(b,c) holds
(Den ((compsym (a,b,c)),A)) . <*g,f*> = F4(a,b,c,g,f) ) )
hereby  ::_thesis: ( ( for a being Element of F1() holds (Den ((idsym a),A)) . {} = F5(a) ) & ( for a, b, c being Element of F1()
for f, g being Element of F2() st f in F3(a,b) & g in F3(b,c) holds
(Den ((compsym (a,b,c)),A)) . <*g,f*> = F4(a,b,c,g,f) ) )
let a, b be Element of F1(); ::_thesis: the Sorts of A . (homsym (a,b)) = F3(a,b)
consider a9, b9 being Element of F1() such that
A43: homsym (a,b) = homsym (a9,b9) and
A44: S . (homsym (a,b)) = F3(a9,b9) by A23;
 a = a9 by A43, Th12;
hence  the Sorts of A . (homsym (a,b)) = F3(a,b) by A43, A44, Th12; ::_thesis: verum
end;
hereby  ::_thesis: for a, b, c being Element of F1()
for f, g being Element of F2() st f in F3(a,b) & g in F3(b,c) holds
(Den ((compsym (a,b,c)),A)) . <*g,f*> = F4(a,b,c,g,f)
let a be Element of F1(); ::_thesis: (Den ((idsym a),A)) . {} = F5(a)
 (idsym a) `1 = 1 by MCART_1:7;
then  ex b being Element of F1() st
( idsym a = idsym b & ex F being Function of {{}},F3(b,b) st
( F = O . (idsym a) & F . {} = F5(b) ) ) by A19;
hence  (Den ((idsym a),A)) . {} = F5(a) by Th11; ::_thesis: verum
end;
let a, b, c be Element of F1(); ::_thesis: for f, g being Element of F2() st f in F3(a,b) & g in F3(b,c) holds
(Den ((compsym (a,b,c)),A)) . <*g,f*> = F4(a,b,c,g,f)
set o = compsym (a,b,c);
 (compsym (a,b,c)) `1 = 2 by MCART_1:7;
then consider a9, b9, c9 being Element of F1() such that
A45: compsym (a,b,c) = compsym (a9,b9,c9) and
A46: ex F being Function of (product <*F3(b9,c9),F3(a9,b9)*>),F3(a9,c9) st
( F = O . (compsym (a,b,c)) & ( for f, g being set st f in F3(a9,b9) & g in F3(b9,c9) holds
F . <*g,f*> = F4(a9,b9,c9,g,f) ) ) by A19;
A47: c = c9 by A45, Th13;
let f, g be Element of F2(); ::_thesis: ( f in F3(a,b) & g in F3(b,c) implies (Den ((compsym (a,b,c)),A)) . <*g,f*> = F4(a,b,c,g,f) )
assume A48: ( f in F3(a,b) & g in F3(b,c) ) ; ::_thesis: (Den ((compsym (a,b,c)),A)) . <*g,f*> = F4(a,b,c,g,f)
 ( a = a9 & b = b9 ) by A45, Th13;
hence  (Den ((compsym (a,b,c)),A)) . <*g,f*> = F4(a,b,c,g,f) by A46, A47, A48; ::_thesis: verum
end;

definition
let C be Category;
func MSAlg C ->  strict MSAlgebra over CatSign the carrier of C means :Def13: :: CATALG_1:def 13
( ( 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
 for b1, b2 being strict MSAlgebra over CatSign the carrier of C st ( for a, b being Object of C holds the Sorts of b1 . (homsym (a,b)) = Hom (a,b) ) & ( for a being Object of C holds (Den ((idsym a),b1)) . {} = 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)),b1)) . <*g,f*> = g (*) f ) & ( for a, b being Object of C holds the Sorts of b2 . (homsym (a,b)) = Hom (a,b) ) & ( for a being Object of C holds (Den ((idsym a),b2)) . {} = 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)),b2)) . <*g,f*> = g (*) f ) holds
b1 = b2
proof
let A1, A2 be strict MSAlgebra over CatSign the carrier of C; ::_thesis: ( ( for a, b being Object of C holds the Sorts of A1 . (homsym (a,b)) = Hom (a,b) ) & ( for a being Object of C holds (Den ((idsym a),A1)) . {} = 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)),A1)) . <*g,f*> = g (*) f ) & ( for a, b being Object of C holds the Sorts of A2 . (homsym (a,b)) = Hom (a,b) ) & ( for a being Object of C holds (Den ((idsym a),A2)) . {} = 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)),A2)) . <*g,f*> = g (*) f ) implies A1 = A2 )
assume 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 ; ::_thesis: A1 = A2
A7: now__::_thesis:_for_i_being_set_st_i_in_the_carrier'_of_(CatSign_the_carrier_of_C)_holds_
the_Charact_of_A1_._i_=_the_Charact_of_A2_._i
let i be set ; ::_thesis: ( i in the carrier' of (CatSign the carrier of C) implies the Charact of A1 . b1 = the Charact of A2 . b1 )
assume  i in the carrier' of (CatSign the carrier of C) ; ::_thesis: the Charact of A1 . b1 = the Charact of A2 . b1
then reconsider o = i as OperSymbol of (CatSign the carrier of C) ;
percases ( o `1 = 1 or o `1 = 2 ) by Th15;
suppose o `1 = 1 ; ::_thesis: the Charact of A1 . b1 = the Charact of A2 . b1
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__::_thesis:_for_x_being_set_st_x_in_{{}}_holds_
(Den_((idsym_a),A1))_._x_=_(Den_((idsym_a),A2))_._x
let x be set ; ::_thesis: ( x in {{}} implies (Den ((idsym a),A1)) . x = (Den ((idsym a),A2)) . x )
assume  x in {{}} ; ::_thesis: (Den ((idsym a),A1)) . x = (Den ((idsym a),A2)) . x
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; ::_thesis: verum
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; ::_thesis: verum
end;
suppose o `1 = 2 ; ::_thesis: the Charact of A1 . b1 = the Charact of A2 . b1
then consider a, b, c being Object of C such that
A15: o = compsym (a,b,c) by Th17;
A16: now__::_thesis:_(_product_<*(Hom_(b,c)),(Hom_(a,b))*>_<>_{}_implies_Hom_(a,c)_<>_{}_)
assume  product <*(Hom (b,c)),(Hom (a,b))*> <> {} ; ::_thesis: Hom (a,c) <> {}
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
 the Element of X = <*g,f*> by FINSEQ_3:124;
reconsider g = g, f = 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; ::_thesis: verum
end;
A21: now__::_thesis:_for_x_being_set_st_x_in_product_<*(Hom_(b,c)),(Hom_(a,b))*>_holds_
(Den_((compsym_(a,b,c)),A1))_._x_=_(Den_((compsym_(a,b,c)),A2))_._x
let x be set ; ::_thesis: ( x in product <*(Hom (b,c)),(Hom (a,b))*> implies (Den ((compsym (a,b,c)),A1)) . x = (Den ((compsym (a,b,c)),A2)) . x )
assume  x in product <*(Hom (b,c)),(Hom (a,b))*> ; ::_thesis: (Den ((compsym (a,b,c)),A1)) . x = (Den ((compsym (a,b,c)),A2)) . x
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 = g, f = 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; ::_thesis: verum
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; ::_thesis: verum
end;
end;
end;
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_(CatSign_the_carrier_of_C)_holds_
the_Sorts_of_A1_._i_=_the_Sorts_of_A2_._i
let i be set ; ::_thesis: ( i in the carrier of (CatSign the carrier of C) implies the Sorts of A1 . i = the Sorts of A2 . i )
assume  i in the carrier of (CatSign the carrier of C) ; ::_thesis: the Sorts of A1 . i = the Sorts of A2 . i
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 ; ::_thesis: verum
end;
then  the Sorts of A1 = the Sorts of A2 by PBOOLE:3;
hence  A1 = A2 by A7, PBOOLE:3; ::_thesis: verum
end;
correctness
existence
ex b1 being strict MSAlgebra over CatSign the carrier of C st
( ( for a, b being Object of C holds the Sorts of b1 . (homsym (a,b)) = Hom (a,b) ) & ( for a being Object of C holds (Den ((idsym a),b1)) . {} = 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)),b1)) . <*g,f*> = g (*) f ) );
proof
deffunc H1( Object of C) ->  Morphism of $1,$1 = id $1;
deffunc H2( Object of C, Object of C, Object of C, Morphism of C, Morphism of C) ->  Element of the carrier' of C = $4 (*) $5;
deffunc H3( Object of C, Object of C) ->  Element of bool the carrier' of C = Hom ($1,$2);
A31: for a being Object of C holds H1(a) in H3(a,a) by CAT_1:27;
A32: now__::_thesis:_for_a,_b,_c_being_Object_of_C
for_f,_g_being_Morphism_of_C_st_f_in_H3(a,b)_&_g_in_H3(b,c)_holds_
H2(a,b,c,g,f)_in_H3(a,c)
let a, b, c be Object of C; ::_thesis: for f, g being Morphism of C st f in H3(a,b) & g in H3(b,c) holds
H2(a,b,c,g,f) in H3(a,c)
let f, g be Morphism of C; ::_thesis: ( f in H3(a,b) & g in H3(b,c) implies H2(a,b,c,g,f) in H3(a,c) )
assume that
A33: f in H3(a,b) and
A34: g in H3(b,c) ; ::_thesis: H2(a,b,c,g,f) in H3(a,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  H2(a,b,c,g,f) in H3(a,c) by A36; ::_thesis: verum
end;
A37: for a, b being Object of C holds H3(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)) = H3(a,b) ) & ( for a being Element of C holds (Den ((idsym a),A)) . {} = H1(a) ) ) and
A39: for a, b, c being Element of C
for f, g being Element of the carrier' of C st f in H3(a,b) & g in H3(b,c) holds
(Den ((compsym (a,b,c)),A)) . <*g,f*> = H2(a,b,c,g,f) from CATALG_1:sch_1(A37, A31, A32);
take  A ; ::_thesis: ( ( for a, b being Object of C holds the Sorts of A . (homsym (a,b)) = Hom (a,b) ) & ( for a being Object of C holds (Den ((idsym a),A)) . {} = 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)),A)) . <*g,f*> = g (*) f ) )
now__::_thesis:_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)),A))_._<*g,f*>_=_g_(*)_f
let a, b, c be Object of C; ::_thesis: 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)),A)) . <*g,f*> = g (*) f
let f, g be Morphism of C; ::_thesis: ( dom f = a & cod f = b & dom g = b & cod g = c implies (Den ((compsym (a,b,c)),A)) . <*g,f*> = g (*) f )
assume  ( dom f = a & cod f = b & dom g = b & cod g = c ) ; ::_thesis: (Den ((compsym (a,b,c)),A)) . <*g,f*> = g (*) f
then  ( f in Hom (a,b) & g in Hom (b,c) ) ;
hence  (Den ((compsym (a,b,c)),A)) . <*g,f*> = g (*) f by A39; ::_thesis: verum
end;
hence  ( ( for a, b being Object of C holds the Sorts of A . (homsym (a,b)) = Hom (a,b) ) & ( for a being Object of C holds (Den ((idsym a),A)) . {} = 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)),A)) . <*g,f*> = g (*) f ) ) by A38; ::_thesis: verum
end;
end;

:: deftheorem Def13 defines MSAlg CATALG_1:def_13_:_
 for C being Category
for b2 being strict MSAlgebra over CatSign the carrier of C holds
( b2 = MSAlg C iff ( ( for a, b being Object of C holds the Sorts of b2 . (homsym (a,b)) = Hom (a,b) ) & ( for a being Object of C holds (Den ((idsym a),b2)) . {} = 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)),b2)) . <*g,f*> = g (*) f ) ) );

theorem Th25: :: CATALG_1:25
for A being Category
for a being Object of A holds Result ((idsym a),(MSAlg A)) = Hom (a,a)
proof
let A be Category; ::_thesis: for a being Object of A holds Result ((idsym a),(MSAlg A)) = Hom (a,a)
let a be Object of A; ::_thesis: Result ((idsym a),(MSAlg A)) = Hom (a,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 ; ::_thesis: verum
end;

theorem Th26: :: CATALG_1:26
for A being Category
for 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; ::_thesis: for 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) )
let a, b, c be Object of A; ::_thesis: ( Args ((compsym (a,b,c)),(MSAlg A)) = product <*(Hom (b,c)),(Hom (a,b))*> & Result ((compsym (a,b,c)),(MSAlg A)) = Hom (a,c) )
 for a, b being Object of A holds the Sorts of (MSAlg A) . (homsym (a,b)) = Hom (a,b) by Def13;
hence  ( Args ((compsym (a,b,c)),(MSAlg A)) = product <*(Hom (b,c)),(Hom (a,b))*> & Result ((compsym (a,b,c)),(MSAlg A)) = Hom (a,c) ) by Lm3; ::_thesis: verum
end;

registration
let C be Category;
cluster MSAlg C ->  strict disjoint_valued feasible ;
coherence
 ( MSAlg C is disjoint_valued & MSAlg C is feasible )
proof
hereby  :: according to PROB_2:def_2,MSAFREE1:def_2 ::_thesis: MSAlg C is feasible
let x, y be set ; ::_thesis: ( x <> y implies not the Sorts of (MSAlg C) . x meets the Sorts of (MSAlg C) . y )
assume that
A1: x <> y and
A2: the Sorts of (MSAlg C) . x meets the Sorts of (MSAlg C) . y ; ::_thesis: contradiction
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 = x, y = 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 = 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; ::_thesis: verum
end;
let o be OperSymbol of (CatSign the carrier of C); :: according to MSUALG_6:def_1 ::_thesis: ( Args (o,(MSAlg C)) = {} or not Result (o,(MSAlg C)) = {} )
percases ( o `1 = 1 or o `1 = 2 ) by Th15;
suppose o `1 = 1 ; ::_thesis: ( Args (o,(MSAlg C)) = {} or not Result (o,(MSAlg C)) = {} )
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  ( Args (o,(MSAlg C)) = {} or not Result (o,(MSAlg C)) = {} ) by CAT_1:27; ::_thesis: verum
end;
suppose o `1 = 2 ; ::_thesis: ( Args (o,(MSAlg C)) = {} or not Result (o,(MSAlg C)) = {} )
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)) <> {} ; ::_thesis: not Result (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) & the Element of Args (o,(MSAlg C)) = <*g,f*> ) by A12, FINSEQ_3:124;
 Result (o,(MSAlg C)) = Hom (a,c) by A11, Th26;
hence  not Result (o,(MSAlg C)) = {} by A13, CAT_1:24; ::_thesis: verum
end;
end;
end;
end;

theorem Th27: :: CATALG_1:27
for C1, C2 being Category
for 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; ::_thesis: for 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)))
let F be Functor of C1,C2; ::_thesis: 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)))
set S1 = CatSign the carrier of C1;
set S2 = CatSign the carrier of C2;
set A1 = MSAlg C1;
set A2 = MSAlg C2;
set f = Upsilon F;
set g = Psi F;
set B1 = (MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F));
set H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1));
let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in the carrier of (CatSign the carrier of C1) or (F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1))) . i is Element of bool [:( the Sorts of (MSAlg C1) . i),( the Sorts of ((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))) . i):] )
assume  i in the carrier of (CatSign the carrier of C1) ; ::_thesis: (F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1))) . i is Element of bool [:( the Sorts of (MSAlg C1) . i),( the Sorts of ((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))) . i):]
then reconsider s = i as SortSymbol of (CatSign the carrier of C1) ;
consider a, b being Object of C1 such that
A1: s = homsym (a,b) by Th14;
 Upsilon F, Psi F form_morphism_between CatSign the carrier of C1, CatSign the carrier of C2 by Th23;
then  the Sorts of ((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))) = the Sorts of (MSAlg C2) * (Upsilon F) by INSTALG1:def_3;
then A2: the Sorts of (MSAlg C2) . ((Upsilon F) . s) = the Sorts of ((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))) . s by FUNCT_2:15;
 (Upsilon F) . s = homsym ((F . a),(F . b)) by A1, Th20;
then A3: the Sorts of (MSAlg C2) . ((Upsilon F) . s) = Hom ((F . a),(F . b)) by Def13;
A4: the Sorts of (MSAlg C1) . s = Hom (a,b) by A1, Def13;
 (F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1))) . s = F | ( the Sorts of (MSAlg C1) . s) by Def1;
then  (F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1))) . s = hom (F,a,b) by A4;
hence  (F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1))) . i is Element of bool [:( the Sorts of (MSAlg C1) . i),( the Sorts of ((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))) . i):] by A2, A4, A3; ::_thesis: verum
end;

theorem Th28: :: CATALG_1:28
for C being Category
for 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; ::_thesis: for 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 ) )
let a, b, c be Object of C; ::_thesis: 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 ) )
let x be set ; ::_thesis: ( 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 ) )
set A = MSAlg C;
 for a, b being Object of C holds the Sorts of (MSAlg C) . (homsym (a,b)) = Hom (a,b) by Def13;
then A1: Args ((compsym (a,b,c)),(MSAlg C)) = product <*(Hom (b,c)),(Hom (a,b))*> by Lm3;
hereby  ::_thesis: ( ex g, f being Morphism of C st
( x = <*g,f*> & dom f = a & cod f = b & dom g = b & cod g = c ) implies x in Args ((compsym (a,b,c)),(MSAlg C)) )
assume  x in Args ((compsym (a,b,c)),(MSAlg C)) ; ::_thesis: ex g, f being Morphism of C st
( x = <*g,f*> & dom f = a & cod f = b & dom g = b & cod g = c )
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 = g, f = f as Morphism of C by A2;
take g = g; ::_thesis: ex f being Morphism of C st
( x = <*g,f*> & dom f = a & cod f = b & dom g = b & cod g = c )
take f = f; ::_thesis: ( x = <*g,f*> & dom f = a & cod f = b & dom g = b & cod g = c )
thus  x = <*g,f*> by A3; ::_thesis: ( dom f = a & cod f = b & dom g = b & cod g = c )
thus  ( dom f = a & cod f = b & dom g = b & cod g = c ) by A2, CAT_1:1; ::_thesis: verum
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 ) ; ::_thesis: x in Args ((compsym (a,b,c)),(MSAlg C))
 ( f in Hom (a,b) & g in Hom (b,c) ) by A5;
hence  x in Args ((compsym (a,b,c)),(MSAlg C)) by A1, A4, FINSEQ_3:124; ::_thesis: verum
end;

theorem Th29: :: CATALG_1:29
for C1, C2 being Category
for 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) holds
for x being Element of Args ((compsym (a,b,c)),(MSAlg C1)) st x = <*g,f*> holds
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; ::_thesis: for 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) holds
for x being Element of Args ((compsym (a,b,c)),(MSAlg C1)) st x = <*g,f*> holds
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)*>
let F be Functor of C1,C2; ::_thesis: 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) holds
for x being Element of Args ((compsym (a,b,c)),(MSAlg C1)) st x = <*g,f*> holds
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)*>
set CS1 = CatSign the carrier of C1;
set CS2 = CatSign the carrier of C2;
set A1 = MSAlg C1;
set A2 = MSAlg C2;
set u = Upsilon F;
set p = Psi F;
set B = (MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F));
let a, b, c be Object of C1; ::_thesis: for f, g being Morphism of C1 st f in Hom (a,b) & g in Hom (b,c) holds
for x being Element of Args ((compsym (a,b,c)),(MSAlg C1)) st x = <*g,f*> holds
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)*>
set o = compsym (a,b,c);
let f, g be Morphism of C1; ::_thesis: ( f in Hom (a,b) & g in Hom (b,c) implies for x being Element of Args ((compsym (a,b,c)),(MSAlg C1)) st x = <*g,f*> holds
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)*> )
assume that
A1: f in Hom (a,b) and
A2: g in Hom (b,c) ; ::_thesis: for x being Element of Args ((compsym (a,b,c)),(MSAlg C1)) st x = <*g,f*> holds
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)*>
let x be Element of Args ((compsym (a,b,c)),(MSAlg C1)); ::_thesis: ( x = <*g,f*> implies 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)*> )
assume A3: x = <*g,f*> ; ::_thesis: 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)*>
 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))),(MSAlg C2)) 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 ((compsym (a,b,c)),(MSAlg C1)) by A3, A6, Th28;
let H be ManySortedFunction of (MSAlg C1),((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))); ::_thesis: ( H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) implies H # x = <*(F . g),(F . f)*> )
assume A8: H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) ; ::_thesis: H # x = <*(F . g),(F . f)*>
 the Sorts of (MSAlg C1) . (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 (MSAlg C1) . (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;
 Upsilon F, Psi F form_morphism_between CatSign the carrier of C1, CatSign the carrier of C2 by Th23;
then A14: Args ((compsym (a,b,c)),((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F)))) = Args (((Psi F) . (compsym (a,b,c))),(MSAlg C2)) by INSTALG1:24
.= Args ((compsym ((F . a),(F . b),(F . c))),(MSAlg C2)) 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 (compsym (a,b,c)) = <*(homsym (b,c)),(homsym (a,b))*> by Def3;
then  ( <*g,f*> . 1 = g & (the_arity_of (compsym (a,b,c))) /. 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 (compsym (a,b,c))) /. 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  H # x = <*(F . g),(F . f)*> by A15, A18, A16, FINSEQ_1:44; ::_thesis: verum
end;

theorem Th30: :: CATALG_1:30
for C being Category
for a, b, c being Object of C
for 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; ::_thesis: for a, b, c being Object of C
for 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
let a, b, c be Object of C; ::_thesis: for 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
let f, g be Morphism of C; ::_thesis: ( f in Hom (a,b) & g in Hom (b,c) implies (Den ((compsym (a,b,c)),(MSAlg C))) . <*g,f*> = g (*) f )
assume that
A1: f in Hom (a,b) and
A2: g in Hom (b,c) ; ::_thesis: (Den ((compsym (a,b,c)),(MSAlg C))) . <*g,f*> = g (*) f
A3: ( dom g = b & cod g = c ) by A2, CAT_1:1;
 ( dom f = a & cod f = b ) by A1, CAT_1:1;
hence  (Den ((compsym (a,b,c)),(MSAlg C))) . <*g,f*> = g (*) f by A3, Def13; ::_thesis: verum
end;

theorem :: CATALG_1:31
for C being Category
for a, b, c, d being Object of C
for 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; ::_thesis: for a, b, c, d being Object of C
for 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*>
let a, b, c, d be Object of C; ::_thesis: for 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*>
let f, g, h be Morphism of C; ::_thesis: ( f in Hom (a,b) & g in Hom (b,c) & h in Hom (c,d) implies (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*> )
assume that
A1: f in Hom (a,b) and
A2: g in Hom (b,c) and
A3: h in Hom (c,d) ; ::_thesis: (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*>
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 ;
::_thesis: verum
end;

theorem :: CATALG_1:32
for C being Category
for a, b being Object of C
for 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; ::_thesis: for a, b being Object of C
for 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 )
let a, b be Object of C; ::_thesis: for 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 )
let f be Morphism of C; ::_thesis: ( f in Hom (a,b) implies ( (Den ((compsym (a,b,b)),(MSAlg C))) . <*(id b),f*> = f & (Den ((compsym (a,a,b)),(MSAlg C))) . <*f,(id a)*> = f ) )
assume A1: f in Hom (a,b) ; ::_thesis: ( (Den ((compsym (a,b,b)),(MSAlg C))) . <*(id b),f*> = f & (Den ((compsym (a,a,b)),(MSAlg C))) . <*f,(id a)*> = f )
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  ( (Den ((compsym (a,b,b)),(MSAlg C))) . <*(id b),f*> = f & (Den ((compsym (a,a,b)),(MSAlg C))) . <*f,(id a)*> = f ) by A1, A3, A2, Th30; ::_thesis: verum
end;

theorem :: CATALG_1:33
for C1, C2 being Category
for 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; ::_thesis: for 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)) )
let F be Functor of C1,C2; ::_thesis: 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)) )
set S1 = CatSign the carrier of C1;
set S2 = CatSign the carrier of C2;
set A1 = MSAlg C1;
set A2 = MSAlg C2;
set f = Upsilon F;
set G = Psi F;
set B1 = (MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F));
A1: Upsilon F, Psi F form_morphism_between CatSign the carrier of C1, CatSign the carrier of C2 by Th23;
reconsider H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) as ManySortedFunction of (MSAlg C1),((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))) by Th27;
take  H ; ::_thesis: ( 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)) )
thus  H = F -MSF ( the carrier of (CatSign the carrier of C1), the Sorts of (MSAlg C1)) ; ::_thesis: H is_homomorphism MSAlg C1,(MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))
let o be OperSymbol of (CatSign the carrier of C1); :: according to MSUALG_3:def_7 ::_thesis: ( Args (o,(MSAlg C1)) = {} or for b1 being Element of Args (o,(MSAlg C1)) holds (H . (the_result_sort_of o)) . ((Den (o,(MSAlg C1))) . b1) = (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # b1) )
assume A2: Args (o,(MSAlg C1)) <> {} ; ::_thesis: for b1 being Element of Args (o,(MSAlg C1)) holds (H . (the_result_sort_of o)) . ((Den (o,(MSAlg C1))) . b1) = (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # b1)
percases ( o `1 = 1 or o `1 = 2 ) by Th15;
suppose o `1 = 1 ; ::_thesis: for b1 being Element of Args (o,(MSAlg C1)) holds (H . (the_result_sort_of o)) . ((Den (o,(MSAlg C1))) . b1) = (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # b1)
then consider a being Object of C1 such that
A3: o = idsym a by Th16;
let x be Element of Args (o,(MSAlg C1)); ::_thesis: (H . (the_result_sort_of o)) . ((Den (o,(MSAlg C1))) . x) = (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # x)
A4: Args (((Psi F) . o),(MSAlg C2)) = Args (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F)))) by A1, INSTALG1:24;
A5: (Psi F) . o = idsym (F . a) by A3, Th21;
then  Args (((Psi F) . o),(MSAlg C2)) = {{}} 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,(MSAlg C1)) = {{}} by A3, Th24;
then  x = {} by TARSKI:def_1;
hence (H . (the_result_sort_of o)) . ((Den (o,(MSAlg C1))) . x) = (H . (the_result_sort_of o)) . h by A3, Def13
.= (H . (homsym (a,a))) . h by A3, Def3
.= (F | ( the Sorts of (MSAlg C1) . (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 (((Psi F) . o),(MSAlg C2))) . (H # x) by A5, A6, Def13
.= (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # x) by Th23, INSTALG1:23 ;
::_thesis: verum
end;
supposeA8: o `1 = 2 ; ::_thesis: for b1 being Element of Args (o,(MSAlg C1)) holds (H . (the_result_sort_of o)) . ((Den (o,(MSAlg C1))) . b1) = (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # b1)
let x be Element of Args (o,(MSAlg C1)); ::_thesis: (H . (the_result_sort_of o)) . ((Den (o,(MSAlg C1))) . x) = (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # x)
consider a, b, c being Object of C1 such that
A9: o = compsym (a,b,c) by A8, Th17;
A10: (Psi F) . 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,(MSAlg C1))) . 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 (MSAlg C1) . (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 (((Psi F) . o),(MSAlg C2))) . <*(F . g),(F . h)*> by A10, A18, A19, Def13
.= (Den (((Psi F) . o),(MSAlg C2))) . (H # x) by A9, A11, A16, Th29
.= (Den (o,((MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F))))) . (H # x) by Th23, INSTALG1:23 ; ::_thesis: verum
end;
end;
end;