inverse_op G is_an_inverseOp_wrt the multF of G by Th22;
hence the multF of G is having_an_inverseOp ; :: thesis: verum