let G be addGroup; :: thesis: (add_inverse G) " = add_inverse G
set f = add_inverse G;
A1: dom (add_inverse G) = the carrier of G by FUNCT_2:def 1;

now :: thesis: for x being object st x in dom (add_inverse G) holds
(add_inverse G) . x = ((add_inverse G) ") . x

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

end;

hence (add_inverse G) " = add_inverse G by A1; :: thesis: verum