set f = a + ;
A1: dom (a +) = the carrier of G by FUNCT_2:def 1;

hereby :: according to FUNCT_1:def 4 :: thesis: a + is onto

let x1, x2 be object ; :: thesis: ( x1 in dom (a +) & x2 in dom (a +) & (a +) . x1 = (a +) . x2 implies x1 = x2 )
assume that
A2: ( x1 in dom (a +) & x2 in dom (a +) ) and
A3: (a +) . x1 = (a +) . x2 ; :: thesis: x1 = x2
reconsider y1 = x1, y2 = x2 as Element of G by A2;
A4: ( (a +) . y1 = a + y1 & (a +) . y2 = a + y2 ) by Def1;
thus x1 = (0_ G) + y1 by Def4
.= ((- a) + a) + y1 by Def5
.= (- a) + (a + y1) by RLVECT_1:def 3
.= ((- a) + a) + y2 by A3, A4, RLVECT_1:def 3
.= (0_ G) + y2 by Def5
.= x2 by Def4 ; :: thesis: verum

end;

thus rng (a +) c= the carrier of G ; :: according to FUNCT_2:def 3,XBOOLE_0:def 10 :: thesis: the carrier of G c= rng (a +)
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of G or y in rng (a +) )
assume y in the carrier of G ; :: thesis: y in rng (a +)
then reconsider y1 = y as Element of G ;
(a +) . ((- a) + y1) = a + ((- a) + y1) by Def1
.= (a + (- a)) + y1 by RLVECT_1:def 3
.= (0_ G) + y1 by Def5
.= y by Def4 ;
hence y in rng (a +) by A1, FUNCT_1:def 3; :: thesis: verum