let IT be multMagma ; :: thesis: ( IT is Group-like implies IT is unital )
assume ex e being Element of IT st
for h being Element of IT holds
( h * e = h & e * h = h & ex g being Element of IT st
( h * g = e & g * h = e ) ) ; :: according to GROUP_1:def 3 :: thesis: IT is unital
hence ex e being Element of IT st
for h being Element of IT holds
( h * e = h & e * h = h ) ; :: according to GROUP_1:def 2 :: thesis: verum