let h1, h2 be Element of G; :: thesis: ( h * h1 = 1_ G & h1 * h = 1_ G & h * h2 = 1_ G & h2 * h = 1_ G implies h1 = h2 )
assume that
A3: ( h * h1 = 1_ G & h1 * h = 1_ G ) and
A4: ( h * h2 = 1_ G & h2 * h = 1_ G ) ; :: thesis: h1 = h2
thus h1 = (1_ G) * h1 by Def5
.= h2 * (h * h1) by A4, Def4
.= h2 by A3, Def5 ; :: thesis: verum