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

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

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

end;

thus (inverse_op G) " = inverse_op G by A1, A2; :: thesis: verum