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 8
.= 1_ H by GROUP_6:40 ;
hence f . ((G ^ o) . g) = (H ^ o) . (f . g) by GROUP_6:def 8; :: thesis: verum