:: deftheorem Def21 defines well-unital MONOID_0:def 21 :
for IT being non empty multLoopStr holds
( IT is well-unital iff 1. IT is_a_unity_wrt the multF of IT );