:: deftheorem Def3 defines UAEndMonoid ENDALG:def 3 :
for UA being Universal_Algebra
for b₂ being strict multLoopStr holds
( b₂ = UAEndMonoid UA iff ( the carrier of b₂ = UAEnd UA & the multF of b₂ = UAEndComp UA & 1. b₂ = id the carrier of UA ) );