let x be object ; :: thesis: ( x in dom (add_inverse G) implies (add_inverse G) . x = ((add_inverse G) ") . x )
assume x in dom (add_inverse G) ; :: thesis: (add_inverse G) . x = ((add_inverse G) ") . x
then reconsider g = x as Element of G ;
A3: (add_inverse G) . (- g) = - (- g) by Def6
.= g ;
thus (add_inverse G) . x = - g by Def6
.= ((add_inverse G) ") . x by A1, A3, FUNCT_1:32 ; :: thesis: verum