for G being addGroup holds add_inverse G is_an_inverseOp_wrt the addF of G