A1: the carrier of A c= the carrier of G by GROUP_2:def 5;
then reconsider f = g | the carrier of A as Function of the carrier of A,the carrier of H by FUNCT_2:38;
f is Homomorphism of A,H

proof

now

let a, b be Element of A; :: thesis: (f . a) * (f . b) = f . (a * b)
A2: ( a is Element of G & b is Element of G ) by A1, TARSKI:def 3;
A3: the multF of G . a,b = a * b

proof

reconsider a' = a as Element of G by A1, TARSKI:def 3;
reconsider b' = b as Element of G by A1, TARSKI:def 3;
thus the multF of G . a,b = a' * b'
.= a * b by GROUP_2:52 ; :: thesis: verum

end;

A4: ( f . a = g . a & f . b = g . b ) by FUNCT_1:72;
for a, b being Element of G holds the multF of H . (g . a),(g . b) = g . (the multF of G . a,b)

proof

let a, b be Element of G; :: thesis: the multF of H . (g . a),(g . b) = g . (the multF of G . a,b)
thus the multF of H . (g . a),(g . b) = (g . a) * (g . b)
.= g . (a * b) by GROUP_6:def 7
.= g . (the multF of G . a,b) ; :: thesis: verum

end;

hence (f . a) * (f . b) = g . (the multF of G . a,b) by A2, A4
.= f . (a * b) by A3, FUNCT_1:72 ;
:: thesis: verum

end;

hence f is Homomorphism of A,H by GROUP_6:def 7; :: thesis: verum

end;

hence g | the carrier of A is Homomorphism of A,H ; :: thesis: verum