:: deftheorem Def6 defines MSAAutComp AUTALG_1:def 6 :
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for b₃ being BinOp of (MSAAut U1) holds
( b₃ = MSAAutComp U1 iff for x, y being Element of MSAAut U1 holds b₃ . (x,y) = y ** x );