thus inverse_op G is one-to-one by Th12; :: thesis: inverse_op G is onto
thus rng (inverse_op G) = the carrier of G by Th13; :: according to FUNCT_2:def 3 :: thesis: verum