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