:: Algebra of Morphisms
:: by Grzegorz Bancerek
::
:: Received January 28, 1997
:: Copyright (c) 1997-2012 Association of Mizar Users


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)
proofend;
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
proofend;
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
proofend;

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))
proofend;

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
proofend;

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
proofend;
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 &amp; b1 is non-empty &amp; b1 is disjoint_valued )
proofend;
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
proofend;
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):] &amp; the carrier' of it = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] &amp; ( for a being set st a in A holds
( the Arity of it . [1,<*a*>] = {} &amp; the ResultSort of it . [1,<*a*>] = [0,<*a,a*>] ) ) &amp; ( for a, b, c being set st a in A &amp; b in A &amp; c in A holds
( the Arity of it . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> &amp; 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):] &amp; the carrier' of b1 = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] &amp; ( for a being set st a in A holds
( the Arity of b1 . [1,<*a*>] = {} &amp; the ResultSort of b1 . [1,<*a*>] = [0,<*a,a*>] ) ) &amp; ( for a, b, c being set st a in A &amp; b in A &amp; c in A holds
( the Arity of b1 . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> &amp; the ResultSort of b1 . [2,<*a,b,c*>] = [0,<*a,c*>] ) ) )
proofend;
correctness
uniqueness
for b1, b2 being strict ManySortedSign st the carrier of b1 = [:{0},(2 -tuples_on A):] &amp; the carrier' of b1 = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] &amp; ( for a being set st a in A holds
( the Arity of b1 . [1,<*a*>] = {} &amp; the ResultSort of b1 . [1,<*a*>] = [0,<*a,a*>] ) ) &amp; ( for a, b, c being set st a in A &amp; b in A &amp; c in A holds
( the Arity of b1 . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> &amp; the ResultSort of b1 . [2,<*a,b,c*>] = [0,<*a,c*>] ) ) &amp; the carrier of b2 = [:{0},(2 -tuples_on A):] &amp; the carrier' of b2 = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] &amp; ( for a being set st a in A holds
( the Arity of b2 . [1,<*a*>] = {} &amp; the ResultSort of b2 . [1,<*a*>] = [0,<*a,a*>] ) ) &amp; ( for a, b, c being set st a in A &amp; b in A &amp; c in A holds
( the Arity of b2 . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> &amp; the ResultSort of b2 . [2,<*a,b,c*>] = [0,<*a,c*>] ) ) holds
b1 = b2;
proofend;
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):] &amp; the carrier' of b2 = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] &amp; ( for a being set st a in A holds
( the Arity of b2 . [1,<*a*>] = {} &amp; the ResultSort of b2 . [1,<*a*>] = [0,<*a,a*>] ) ) &amp; ( for a, b, c being set st a in A &amp; b in A &amp; c in A holds
( the Arity of b2 . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> &amp; 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
proofend;
end;

registration
let A be non empty set ;
cluster CatSign A ->  non empty non void strict ;
coherence
 ( not CatSign A is empty &amp; not CatSign A is void )
proofend;
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 &amp; 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 &amp; 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
proofend;
end;

registration
cluster non empty strict feasible Categorial for ManySortedSign ;
existence
 ex b1 being Signature st
( b1 is Categorial &amp; not b1 is empty &amp; b1 is strict )
proofend;
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 &amp; the carrier of it = [:{0},(2 -tuples_on A):] );
existence
 ex b1 being Signature st
( CatSign A is Subsignature of b1 &amp; the carrier of b1 = [:{0},(2 -tuples_on A):] )
proofend;
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 &amp; 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
proofend;

registration
let A be set ;
cluster  ->  Categorial for CatSignature of A;
coherence
 for b1 being CatSignature of A holds b1 is Categorial
proofend;
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
proofend;
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
proofend;
end;

definition
let A be set ;
:: original:CatSign
redefine func CatSign A ->  strict CatSignature of A;
coherence
 CatSign A is strict CatSignature of A
proofend;
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 &amp; 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 &amp; x in rng f ) )
proofend;
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 &amp; x in rng f ) ) ) &amp; ( 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 &amp; x in rng f ) ) ) holds
b1 = b2
proofend;
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 &amp; x in rng f ) ) );

theorem Th5: :: CATALG_1:5
for A being set holds underlay (CatSign A) = A
proofend;

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] &amp; len p = f . i &amp; [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier of S ) ) &amp; ( 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] &amp; len p = f . i &amp; [:{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] &amp; len p = f . i &amp; [:{i},((f . i) -tuples_on (underlay S)):] c= the carrier of S ) ) &amp; ( 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] &amp; len p = f . i &amp; [:{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
proofend;
end;

registration
cluster non empty strict feasible Categorial delta-concrete for ManySortedSign ;
existence
 ex b1 being CatSignature st
( b1 is delta-concrete &amp; not b1 is empty &amp; b1 is strict )
proofend;
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 &amp; b1 is strict )
proofend;
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] &amp; rng p c= underlay S )
proofend;

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 &amp; [i,p2] in the carrier of S ) or ( [i,p1] in the carrier' of S &amp; [i,p2] in the carrier' of S ) ) holds
len p1 = len p2
proofend;

theorem :: CATALG_1:8
for S being delta-concrete ManySortedSign
for i being set
for p1, p2 being FinSequence st len p2 = len p1 &amp; rng p2 c= underlay S holds
( ( [i,p1] in the carrier of S implies [i,p2] in the carrier of S ) &amp; ( [i,p1] in the carrier' of S implies [i,p2] in the carrier' of S ) )
proofend;

theorem :: CATALG_1:9
for S being non empty Categorial delta-concrete Signature holds S is CatSignature of underlay S
proofend;

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 &amp; s `2 is Function-like )
proofend;
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 &amp; s `2 is Function-like )
proofend;
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 &amp; o `2 is Function-like )
proofend;
end;

registration
let S be non empty CatSignature;
let s be SortSymbol of S;
clusters `2  ->  FinSequence-like ;
coherence
 s `2 is FinSequence-like
proofend;
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
proofend;
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
proofend;
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 &amp; ( for b being Element of A holds
( homsym (a,b) in the carrier of S &amp; ( for c being Element of A holds compsym (a,b,c) in the carrier' of S ) ) ) )
proofend;

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
proofend;

theorem Th12: :: CATALG_1:12
for a1, b1, a2, b2 being set st homsym (a1,a2) = homsym (b1,b2) holds
( a1 = b1 &amp; a2 = b2 )
proofend;

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 &amp; a2 = b2 &amp; a3 = b3 )
proofend;

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)
proofend;

theorem Th15: :: CATALG_1:15
for A being non empty set
for o being OperSymbol of (CatSign A) holds
( ( o `1 = 1 &amp; len (o `2) = 1 ) or ( o `1 = 2 &amp; len (o `2) = 3 ) )
proofend;

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
proofend;

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)
proofend;

theorem :: CATALG_1:18
for A being non empty set
for a being Element of A holds
( the_arity_of (idsym a) = {} &amp; 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))*> &amp; 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))] ) &amp; ( for s being SortSymbol of (CatSign the carrier of C1) holds b2 . s = [0,((Obj F) * (s `2))] ) holds
b1 = b2
proofend;
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))]
proofend;
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))] ) &amp; ( for o being OperSymbol of (CatSign the carrier of C1) holds b2 . o = [(o `1),((Obj F) * (o `2))] ) holds
b1 = b2
proofend;
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))]
proofend;
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} &amp; {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} &amp; <*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))
proofend;

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)
proofend;

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))
proofend;

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
proofend;

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) = {{}}
proofend;

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))*> &amp; Result ((compsym (a,b,c)),A) = Hom (a,c) )
proofend;

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) ) &amp; ( for a being Element of F1() holds (Den ((idsym a),A)) . {} = F5(a) ) &amp; ( for a, b, c being Element of F1()
for f, g being Element of F2() st f in F3(a,b) &amp; 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) &amp; g in F3(b,c) holds
F4(a,b,c,g,f) in F3(a,c)
proofend;

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) ) &amp; ( for a being Object of C holds (Den ((idsym a),it)) . {} = id a ) &amp; ( for a, b, c being Object of C
for f, g being Morphism of C st dom f = a &amp; cod f = b &amp; dom g = b &amp; 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) ) &amp; ( for a being Object of C holds (Den ((idsym a),b1)) . {} = id a ) &amp; ( for a, b, c being Object of C
for f, g being Morphism of C st dom f = a &amp; cod f = b &amp; dom g = b &amp; cod g = c holds
(Den ((compsym (a,b,c)),b1)) . <*g,f*> = g (*) f ) &amp; ( for a, b being Object of C holds the Sorts of b2 . (homsym (a,b)) = Hom (a,b) ) &amp; ( for a being Object of C holds (Den ((idsym a),b2)) . {} = id a ) &amp; ( for a, b, c being Object of C
for f, g being Morphism of C st dom f = a &amp; cod f = b &amp; dom g = b &amp; cod g = c holds
(Den ((compsym (a,b,c)),b2)) . <*g,f*> = g (*) f ) holds
b1 = b2
proofend;
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) ) &amp; ( for a being Object of C holds (Den ((idsym a),b1)) . {} = id a ) &amp; ( for a, b, c being Object of C
for f, g being Morphism of C st dom f = a &amp; cod f = b &amp; dom g = b &amp; cod g = c holds
(Den ((compsym (a,b,c)),b1)) . <*g,f*> = g (*) f ) );
proofend;
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) ) &amp; ( for a being Object of C holds (Den ((idsym a),b2)) . {} = id a ) &amp; ( for a, b, c being Object of C
for f, g being Morphism of C st dom f = a &amp; cod f = b &amp; dom g = b &amp; 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)
proofend;

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))*> &amp; Result ((compsym (a,b,c)),(MSAlg A)) = Hom (a,c) )
proofend;

registration
let C be Category;
cluster MSAlg C ->  strict disjoint_valued feasible ;
coherence
 ( MSAlg C is disjoint_valued &amp; MSAlg C is feasible )
proofend;
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)))
proofend;

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*> &amp; dom f = a &amp; cod f = b &amp; dom g = b &amp; cod g = c ) )
proofend;

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) &amp; 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)*>
proofend;

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) &amp; g in Hom (b,c) holds
(Den ((compsym (a,b,c)),(MSAlg C))) . <*g,f*> = g (*) f
proofend;

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) &amp; g in Hom (b,c) &amp; 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*>
proofend;

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 &amp; (Den ((compsym (a,a,b)),(MSAlg C))) . <*f,(id a)*> = f )
proofend;

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)) &amp; H is_homomorphism MSAlg C1,(MSAlg C2) | ((CatSign the carrier of C1),(Upsilon F),(Psi F)) )
proofend;