:: deftheorem Def10 defines unital MONOID_0:def 10 :
for IT being non empty multMagma holds
( IT is unital iff the multF of IT is having_a_unity );