for G being AbGroup holds comp G is_an_inverseOp_wrt the addF of G