now :: thesis: for g, h being Element of (H . i) holds (injection (H,i)) . (g * h) = ((injection (H,i)) . g) * ((injection (H,i)) . h)

let g, h be Element of (H . i); :: thesis: (injection (H,i)) . (g * h) = ((injection (H,i)) . g) * ((injection (H,i)) . h)
thus (injection (H,i)) . (g * h) = [*i,(g * h)*] by Th56
.= [*i,g*] * [*i,h*] by Th51
.= ((injection (H,i)) . g) * [*i,h*] by Th56
.= ((injection (H,i)) . g) * ((injection (H,i)) . h) by Th56 ; :: thesis: verum

end;

hence injection (H,i) is multiplicative by GROUP_6:def 6; :: thesis: injection (H,i) is one-to-one

now :: thesis: for x1, x2 being object st x1 in dom (injection (H,i)) & x2 in dom (injection (H,i)) & (injection (H,i)) . x1 = (injection (H,i)) . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom (injection (H,i)) & x2 in dom (injection (H,i)) & (injection (H,i)) . x1 = (injection (H,i)) . x2 implies x1 = x2 )
assume ( x1 in dom (injection (H,i)) & x2 in dom (injection (H,i)) ) ; :: thesis: ( (injection (H,i)) . x1 = (injection (H,i)) . x2 implies x1 = x2 )
then reconsider g1 = x1, g2 = x2 as Element of (H . i) ;
assume (injection (H,i)) . x1 = (injection (H,i)) . x2 ; :: thesis: x1 = x2
then [*i,g1*] = (injection (H,i)) . x2 by Th56
.= [*i,g2*] by Th56 ;
then ( ( i = i & g1 = g2 ) or ( g1 = 1_ (H . i) & g2 = 1_ (H . i) ) ) by Th50;
hence x1 = x2 ; :: thesis: verum

end;

hence injection (H,i) is one-to-one by FUNCT_1:def 4; :: thesis: verum