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