let G be addGroup; :: thesis: the_inverseOp_wrt the addF of G = add_inverse G
set o = the addF of G;
( the addF of G is having_an_inverseOp & add_inverse G is_an_inverseOp_wrt the addF of G ) by Th22;
hence the_inverseOp_wrt the addF of G = add_inverse G by FINSEQOP:def 3; :: thesis: verum