:: deftheorem Def5 defines MSAEndComp ENDALG:def 5 :
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for b₃ being BinOp of (MSAEnd U1) holds
( b₃ = MSAEndComp U1 iff for x, y being Element of MSAEnd U1 holds b₃ . (x,y) = y ** x );