set H = multMagma(# the carrier of G, the multF of G #);
reconsider e = 1_ G as Element of multMagma(# the carrier of G, the multF of G #) ;
take e ; :: according to GROUP_1:def 2 :: thesis: for h being Element of multMagma(# the carrier of G, the multF of G #) holds
( h * e = h & e * h = h & ex g being Element of multMagma(# the carrier of G, the multF of G #) st
( h * g = e & g * h = e ) )
let h be Element of multMagma(# the carrier of G, the multF of G #); :: thesis: ( h * e = h & e * h = h & ex g being Element of multMagma(# the carrier of G, the multF of G #) st
( h * g = e & g * h = e ) )
reconsider h9 = h as Element of G ;
thus h * e = h9 * (1_ G)
.= h by Def4 ; :: thesis: ( e * h = h & ex g being Element of multMagma(# the carrier of G, the multF of G #) st
( h * g = e & g * h = e ) )
thus e * h = (1_ G) * h9
.= h by Def4 ; :: thesis: ex g being Element of multMagma(# the carrier of G, the multF of G #) st
( h * g = e & g * h = e )
reconsider g = h9 " as Element of multMagma(# the carrier of G, the multF of G #) ;
take g ; :: thesis: ( h * g = e & g * h = e )
thus h * g = h9 * (h9 ")
.= e by Def5 ; :: thesis: g * h = e
thus g * h = (h9 ") * h9
.= e by Def5 ; :: thesis: verum