let M be non empty unital multMagma ; :: thesis: ( ( for h being Element of M ex g being Element of M st
( h * g = 1_ M & g * h = 1_ M ) ) implies M is Group-like )
assume A1: for h being Element of M ex g being Element of M st
( h * g = 1_ M & g * h = 1_ M ) ; :: thesis: M is Group-like
ex e being Element of M st
for h being Element of M holds
( h * e = h & e * h = h & ex g being Element of M st
( h * g = e & g * h = e ) )

proof

take e = 1_ M; :: thesis: for h being Element of M holds
( h * e = h & e * h = h & ex g being Element of M st
( h * g = e & g * h = e ) )
let h be Element of M; :: thesis: ( h * e = h & e * h = h & ex g being Element of M st
( h * g = e & g * h = e ) )
thus h * e = h by GROUP_1:def 4; :: thesis: ( e * h = h & ex g being Element of M st
( h * g = e & g * h = e ) )
thus e * h = h by GROUP_1:def 4; :: thesis: ex g being Element of M st
( h * g = e & g * h = e )
thus ex g being Element of M st
( h * g = e & g * h = e ) by A1; :: thesis: verum

end;

hence M is Group-like ; :: thesis: verum