set f = 1: (G,H);
let a, b be Element of G; :: according to GROUP_6:def 6 :: 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 ;
hence (1: (G,H)) . (a * b) = ((1: (G,H)) . a) * ((1: (G,H)) . b) by Lm1; :: thesis: verum