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