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 = 1_ G & g * h = 1_ G )
thus ( h * g = 1_ G & g * h = 1_ G ) by A1, A2, Def4; :: thesis: verum