let e1, e2 be Element of G; :: thesis: ( ( for h being Element of G holds
( h * e1 = h & e1 * h = h ) ) & ( for h being Element of G holds
( h * e2 = h & e2 * h = h ) ) implies e1 = e2 )
assume that
A2: for h being Element of G holds
( h * e1 = h & e1 * h = h ) and
A3: for h being Element of G holds
( h * e2 = h & e2 * h = h ) ; :: thesis: e1 = e2
thus e1 = e2 * e1 by A3
.= e2 by A2 ; :: thesis: verum