set f = incl1 (G,A,phi);
for g1, g2 being Element of G holds (incl1 (G,A,phi)) . (g1 * g2) = ((incl1 (G,A,phi)) . g1) * ((incl1 (G,A,phi)) . g2)

proof

let g1, g2 be Element of G; :: thesis: (incl1 (G,A,phi)) . (g1 * g2) = ((incl1 (G,A,phi)) . g1) * ((incl1 (G,A,phi)) . g2)
( (incl1 (G,A,phi)) . g1 = <*g1,(1_ A)*> & (incl1 (G,A,phi)) . g2 = <*g2,(1_ A)*> & (incl1 (G,A,phi)) . (g1 * g2) = <*(g1 * g2),(1_ A)*> ) by Def2;
hence (incl1 (G,A,phi)) . (g1 * g2) = ((incl1 (G,A,phi)) . g1) * ((incl1 (G,A,phi)) . g2) by Th23; :: thesis: verum

end;

hence incl1 (G,A,phi) is multiplicative by GROUP_6:def 6; :: thesis: incl1 (G,A,phi) is one-to-one
for g1, g2 being Element of G st (incl1 (G,A,phi)) . g1 = (incl1 (G,A,phi)) . g2 holds
g1 = g2

proof

let g1, g2 be Element of G; :: thesis: ( (incl1 (G,A,phi)) . g1 = (incl1 (G,A,phi)) . g2 implies g1 = g2 )
assume A1: (incl1 (G,A,phi)) . g1 = (incl1 (G,A,phi)) . g2 ; :: thesis: g1 = g2
<*g1,(1_ A)*> = (incl1 (G,A,phi)) . g1 by Def2
.= <*g2,(1_ A)*> by A1, Def2 ;
hence g1 = g2 by FINSEQ_1:77; :: thesis: verum

end;

hence incl1 (G,A,phi) is one-to-one by GROUP_6:1; :: thesis: verum