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

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