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