set f = incl2 (G,A,phi);
for a1, a2 being Element of A holds (incl2 (G,A,phi)) . (a1 * a2) = ((incl2 (G,A,phi)) . a1) * ((incl2 (G,A,phi)) . a2)

proof

let a1, a2 be Element of A; :: thesis: (incl2 (G,A,phi)) . (a1 * a2) = ((incl2 (G,A,phi)) . a1) * ((incl2 (G,A,phi)) . a2)
( (incl2 (G,A,phi)) . a1 = <*(1_ G),a1*> & (incl2 (G,A,phi)) . a2 = <*(1_ G),a2*> & (incl2 (G,A,phi)) . (a1 * a2) = <*(1_ G),(a1 * a2)*> ) by Def3;
hence (incl2 (G,A,phi)) . (a1 * a2) = ((incl2 (G,A,phi)) . a1) * ((incl2 (G,A,phi)) . a2) by Th26; :: thesis: verum

end;

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

proof

let a1, a2 be Element of A; :: thesis: ( (incl2 (G,A,phi)) . a1 = (incl2 (G,A,phi)) . a2 implies a1 = a2 )
assume A1: (incl2 (G,A,phi)) . a1 = (incl2 (G,A,phi)) . a2 ; :: thesis: a1 = a2
<*(1_ G),a1*> = (incl2 (G,A,phi)) . a1 by Def3
.= <*(1_ G),a2*> by A1, Def3 ;
hence a1 = a2 by FINSEQ_1:77; :: thesis: verum

end;

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