for G being non empty addGroup-like addMagma
for e being Element of G st ( for h being Element of G holds
( h + e = h & e + h = h ) ) holds
e = 0_ G by Def4;