set f = 1: (G,H);
reconsider f = 1: (G,H) as Function of G,H ;
take f ; :: thesis: ( f is multiplicative & f is homomorphic )
thus f is multiplicative ; :: thesis: f is homomorphic
let o be Element of O; :: according to GROUP_9:def 18 :: thesis: for g being Element of G holds f . ((G ^ o) . g) = (H ^ o) . (f . g)
let g be Element of G; :: thesis: f . ((G ^ o) . g) = (H ^ o) . (f . g)
(H ^ o) . (f . g) = (H ^ o) . (1_ H) by GROUP_6:def 7
.= 1_ H by GROUP_6:31 ;
hence f . ((G ^ o) . g) = (H ^ o) . (f . g) by GROUP_6:def 7; :: thesis: verum