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

hereby :: according to FUNCT_1:def 8 :: thesis: a * is onto

let x1, x2 be set ; :: thesis: ( x1 in dom (a * ) & x2 in dom (a * ) & (a * ) . x1 = (a * ) . x2 implies x1 = x2 )
assume A2: ( x1 in dom (a * ) & x2 in dom (a * ) & (a * ) . x1 = (a * ) . x2 ) ; :: thesis: x1 = x2
then reconsider y1 = x1, y2 = x2 as Element of G ;
A3: ( (a * ) . y1 = a * y1 & (a * ) . y2 = a * y2 ) by Def1;
thus x1 = (1_ G) * y1 by GROUP_1:def 5
.= ((a " ) * a) * y1 by GROUP_1:def 6
.= (a " ) * (a * y1) by GROUP_1:def 4
.= ((a " ) * a) * y2 by A2, A3, GROUP_1:def 4
.= (1_ G) * y2 by GROUP_1:def 6
.= x2 by GROUP_1:def 5 ; :: 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 set ; :: 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 4
.= (1_ G) * y1 by GROUP_1:def 6
.= y by GROUP_1:def 5 ;
hence y in rng (a * ) by A1, FUNCT_1:def 5; :: thesis: verum