let G be Group; :: thesis: rng (inverse_op G) = the carrier of G
set f = inverse_op G;
thus rng (inverse_op G) c= the carrier of G ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of G c= rng (inverse_op G)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of G or x in rng (inverse_op G) )
A1: dom (inverse_op G) = the carrier of G by FUNCT_2:def 1;
assume x in the carrier of G ; :: thesis: x in rng (inverse_op G)
then reconsider a = x as Element of G ;
(inverse_op G) . (a ") = (a ") " by GROUP_1:def 6
.= a ;
hence x in rng (inverse_op G) by A1, FUNCT_1:def 3; :: thesis: verum