theorem :: GROUP_1:24

for G being Group holds the_inverseOp_wrt the multF of G = inverse_op G