let G be Group; :: thesis: the multF of G is having_an_inverseOp
inverse_op G is_an_inverseOp_wrt the multF of G by Th35;
hence the multF of G is having_an_inverseOp by FINSEQOP:def 2; :: thesis: verum