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