:: deftheorem Def2 defines +* CIRCCOMB:def 2 :
for S1, S2 being non empty ManySortedSign
for b₃ being non empty strict ManySortedSign holds
( b₃ = S1 +* S2 iff ( the carrier of b₃ = the carrier of S1 \/ the carrier of S2 & the carrier' of b₃ = the carrier' of S1 \/ the carrier' of S2 & the Arity of b₃ = the Arity of S1 +* the Arity of S2 & the ResultSort of b₃ = the ResultSort of S1 +* the ResultSort of S2 ) );