take f = G --> (1_ H); :: thesis: f is multiplicative
for a being Element of G holds f . a = 1_ H ;
hence for a, b being Element of G holds f . (a * b) = (f . a) * (f . b) by Lm1; :: according to GROUP_6:def 6 :: thesis: verum