:: deftheorem Def2 defines UAAutComp AUTALG_1:def 2 :
for UA being Universal_Algebra
for b₂ being BinOp of (UAAut UA) holds
( b₂ = UAAutComp UA iff for x, y being Element of UAAut UA holds b₂ . (x,y) = y * x );