set f = + a;
A5: 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
A6: ( x1 in dom (+ a) & x2 in dom (+ a) ) and
A7: (+ a) . x1 = (+ a) . x2 ; :: thesis: x1 = x2
reconsider y1 = x1, y2 = x2 as Element of G by A6;
A8: ( (+ a) . y1 = y1 + a & (+ a) . y2 = y2 + a ) by Def2;
thus x1 = y1 + (0_ G) by Def4
.= y1 + (a + (- a)) by Def5
.= (y1 + a) + (- a) by RLVECT_1:def 3
.= y2 + (a + (- a)) by A7, A8, RLVECT_1:def 3
.= y2 + (0_ G) 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) . (y1 + (- a)) = (y1 + (- a)) + a by Def2
.= y1 + ((- a) + a) by RLVECT_1:def 3
.= y1 + (0_ G) by Def5
.= y by Def4 ;
hence y in rng (+ a) by A5, FUNCT_1:def 3; :: thesis: verum