reconsider f = the carrier of G --> (1_ H) as Function of G,H ;
for a being Element of G holds f . a = 1_ H by FUNCOP_1:7;
then for a, b being Element of G holds f . (a * b) = (f . a) * (f . b) by Lm1;
then reconsider g = f as Homomorphism of G,H by Def7;
take g ; :: thesis: for a being Element of G holds g . a = 1_ H
thus for a being Element of G holds g . a = 1_ H by FUNCOP_1:7; :: thesis: verum