:: deftheorem Def6 defines MSAEndMonoid ENDALG:def 6 :
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for b₃ being strict multLoopStr holds
( b₃ = MSAEndMonoid U1 iff ( the carrier of b₃ = MSAEnd U1 & the multF of b₃ = MSAEndComp U1 & 1. b₃ = id the Sorts of U1 ) );