for G being addGroup holds rng (add_inverse G) = the carrier of G