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