set f = id the carrier of H;
id the carrier of H is Function of the carrier of H, the carrier of G

proof

B1: dom (id the carrier of H) = the carrier of H ;
rng (id the carrier of H) c= the carrier of G by A1, GROUP_2:def 5;
hence id the carrier of H is Function of the carrier of H, the carrier of G by B1, FUNCT_2:2; :: thesis: verum

end;

then reconsider f = id the carrier of H as Function of H,G ;
for g, h being Element of H holds f . (g * h) = (f . g) * (f . h) by A1, GROUP_2:43;
hence id the carrier of H is Homomorphism of H,G by GROUP_6:def 6; :: thesis: verum