consider e being Element of G such that
A1: for h being Element of G holds
( h + e = h & e + h = h & ex g being Element of G st
( h + g = e & g + h = e ) ) by Def2;
consider g being Element of G such that
A2: ( h + g = e & g + h = e ) by A1;
take g ; :: thesis: ( h + g = 0_ G & g + h = 0_ G )
thus ( h + g = 0_ G & g + h = 0_ G ) by A1, A2, Def4; :: thesis: verum