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

let x be set ; :: 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 7
.= g ;
thus (inverse_op G) . x = g " by GROUP_1:def 7
.= ((inverse_op G) " ) . x by A1, A3, FUNCT_1:54 ; :: thesis: verum

end;

dom ((inverse_op G) " ) = the carrier of G by FUNCT_2:def 1;
hence (inverse_op G) " = inverse_op G by A1, A2, FUNCT_1:9; :: thesis: verum