:: deftheorem defines unital GROUP_1:def 1 :
for IT being multMagma holds
( IT is unital iff ex e being Element of IT st
for h being Element of IT holds
( h * e = h & e * h = h ) );