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