for G being Group holds inverse_op G is_an_inverseOp_wrt the multF of G