set H = multMagma(# the carrier of G,the multF of G #);
reconsider e = 1_ G as Element of ;
take e ; :: according to GROUP_1:def 3 :: thesis: for b₁ being Element of the carrier of multMagma(# the carrier of G,the multF of G #) holds
( b₁ * e = b₁ & e * b₁ = b₁ & ex b₂ being Element of the carrier of multMagma(# the carrier of G,the multF of G #) st
( b₁ * b₂ = e & b₂ * b₁ = e ) )
let h be Element of ; :: thesis: ( h * e = h & e * h = h & ex b₁ being Element of the carrier of multMagma(# the carrier of G,the multF of G #) st
( h * b₁ = e & b₁ * h = e ) )
reconsider h' = h as Element of ;
thus h * e = h' * (1_ G)
.= h by GROUP_1:def 5 ; :: thesis: ( e * h = h & ex b₁ being Element of the carrier of multMagma(# the carrier of G,the multF of G #) st
( h * b₁ = e & b₁ * h = e ) )
thus e * h = (1_ G) * h'
.= h by GROUP_1:def 5 ; :: thesis: ex b₁ being Element of the carrier of multMagma(# the carrier of G,the multF of G #) st
( h * b₁ = e & b₁ * h = e )
reconsider g = h' " as Element of ;
take g ; :: thesis: ( h * g = e & g * h = e )
thus h * g = h' * (h' " )
.= e by GROUP_1:def 6 ; :: thesis: g * h = e
thus g * h = (h' " ) * h'
.= e by GROUP_1:def 6 ; :: thesis: verum