:: deftheorem Def1 defines unital TOPALG_7:def 1 :
for G being multMagma
for g being Element of G holds
( g is unital iff g = 1_ G );