take f = 1: (G,H); :: 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 FUNCOP_1:7
.= 1_ H by GROUP_6:31 ;
hence f . ((G ^ o) . g) = (H ^ o) . (f . g) by FUNCOP_1:7; :: thesis: verum