:: deftheorem Def4 defines +* CIRCCOMB:def 4 :
for S1, S2 being non empty ManySortedSign
for A1 being non-empty MSAlgebra over S1
for A2 being non-empty MSAlgebra over S2 st the Sorts of A1 tolerates the Sorts of A2 holds
for b₅ being strict non-empty MSAlgebra over S1 +* S2 holds
( b₅ = A1 +* A2 iff ( the Sorts of b₅ = the Sorts of A1 +* the Sorts of A2 & the Charact of b₅ = the Charact of A1 +* the Charact of A2 ) );