:: deftheorem Def3 defines CatSign CATALG_1:def 3 :
for A being set
for b₂ being strict ManySortedSign holds
( b₂ = CatSign A iff ( the carrier of b₂ = [:{0},(2 -tuples_on A):] & the carrier' of b₂ = [:{1},(1 -tuples_on A):] \/ [:{2},(3 -tuples_on A):] & ( for a being set st a in A holds
( the Arity of b₂ . [1,<*a*>] = {} & the ResultSort of b₂ . [1,<*a*>] = [0,<*a,a*>] ) ) & ( for a, b, c being set st a in A & b in A & c in A holds
( the Arity of b₂ . [2,<*a,b,c*>] = <*[0,<*b,c*>],[0,<*a,b*>]*> & the ResultSort of b₂ . [2,<*a,b,c*>] = [0,<*a,c*>] ) ) ) );