for G being addGroup holds (add_inverse G) " = add_inverse G