:: deftheorem Def4 defines MSAlgCat MSINST_1:def 4 :
for S being non empty non void ManySortedSign
for A being non empty set
for b₃ being non empty strict AltCatStr holds
( b₃ = MSAlgCat (S,A) iff ( the carrier of b₃ = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of b₃ . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being Object of b₃
for f, g being Function-yielding Function st f in the Arrows of b₃ . (i,j) & g in the Arrows of b₃ . (j,k) holds
( the Comp of b₃ . (i,j,k)) . (g,f) = g ** f ) ) );