:: deftheorem Def1 defines MSSCat MSINST_1:def 1 :
for A being non empty set
for b₂ being non empty strict AltCatStr holds
( b₂ = MSSCat A iff ( the carrier of b₂ = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of b₂ . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being Object of b₂ st i in MSS_set A & j in MSS_set A & k in MSS_set A holds
for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of b₂ . (i,j) & [g1,g2] in the Arrows of b₂ . (j,k) holds
( the Comp of b₂ . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) ) );