scheme :: CATALG_1:sch 1
CatAlgEx{ F₁() -> non empty set , F₂() -> non empty set , F₃( set , set ) -> set , F₄( set , set , set , object , object ) -> set , F₅( set ) -> set } :

ex A being strict MSAlgebra over CatSign F₁() st
( ( for a, b being Element of F₁() holds the Sorts of A . (homsym (a,b)) = F₃(a,b) ) & ( for a being Element of F₁() holds (Den ((idsym a),A)) . {} = F₅(a) ) & ( for a, b, c being Element of F₁()
for f, g being Element of F₂() st f in F₃(a,b) & g in F₃(b,c) holds
(Den ((compsym (a,b,c)),A)) . <*g,f*> = F₄(a,b,c,g,f) ) )

provided

A1: for a, b being Element of F₁() holds F₃(a,b) c= F₂() and
A2: for a being Element of F₁() holds F₅(a) in F₃(a,a) and
A3: for a, b, c being Element of F₁()
for f, g being Element of F₂() st f in F₃(a,b) & g in F₃(b,c) holds
F₄(a,b,c,g,f) in F₃(a,c)