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 = (1_ G) * y1 by GROUP_1:def 4
.= ((a ") * a) * y1 by GROUP_1:def 5
.= (a ") * (a * y1) by GROUP_1:def 3
.= ((a ") * a) * y2 by A3, A4, GROUP_1:def 3
.= (1_ G) * y2 by GROUP_1:def 5
.= x2 by GROUP_1:def 4 ; :: 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 GROUP_1:def 3
.= (1_ G) * y1 by GROUP_1:def 5
.= y by GROUP_1:def 4 ;
hence y in rng (a *) by A1, FUNCT_1:def 3; :: thesis: verum