set f = * a;
A4: 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 A5: ( 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 ;
A6: ( (* a) . y1 = y1 * a & (* a) . y2 = y2 * a ) by Def2;
thus x1 = y1 * (1_ G) by GROUP_1:def 5
.= y1 * (a * (a " )) by GROUP_1:def 6
.= (y1 * a) * (a " ) by GROUP_1:def 4
.= y2 * (a * (a " )) by A5, A6, GROUP_1:def 4
.= y2 * (1_ G) 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) . (y1 * (a " )) = (y1 * (a " )) * a by Def2
.= y1 * ((a " ) * a) by GROUP_1:def 4
.= y1 * (1_ G) by GROUP_1:def 6
.= y by GROUP_1:def 5 ;
hence y in rng (* a) by A4, FUNCT_1:def 5; :: thesis: verum