set f = 1: (G,H);
let a be Element of G; :: according to GROUP_6:def 6 :: thesis: for b being Element of G holds (1: (G,H)) . (a * b) = ((1: (G,H)) . a) * ((1: (G,H)) . b)
let b be Element of G; :: thesis: (1: (G,H)) . (a * b) = ((1: (G,H)) . a) * ((1: (G,H)) . b)
for a being Element of G holds (1: (G,H)) . a = 1_ H by FUNCOP_1:7;
hence (1: (G,H)) . (a * b) = ((1: (G,H)) . a) * ((1: (G,H)) . b) by Lm1; :: thesis: verum