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