reconsider m = the carrier of G --> (1. H) as Function of the carrier of G, the carrier of H ;

reconsider m = m as Function of G,H ;

take m ; :: thesis: ( m is multiplicative & m is unity-preserving )

for x, y being Element of G holds m . (x * y) = (m . x) * (m . y)

thus m . (1_ G) = 1_ H by FUNCOP_1:7; :: according to GROUP_1:def 13 :: thesis: verum

reconsider m = m as Function of G,H ;

take m ; :: thesis: ( m is multiplicative & m is unity-preserving )

for x, y being Element of G holds m . (x * y) = (m . x) * (m . y)

proof

hence
m is multiplicative
by GROUP_6:def 6; :: thesis: m is unity-preserving
let x, y be Element of G; :: thesis: m . (x * y) = (m . x) * (m . y)

m . (x * y) = 1. H by FUNCOP_1:7

.= (1. H) * (1. H)

.= (m . x) * (1. H) by FUNCOP_1:7

.= (m . x) * (m . y) by FUNCOP_1:7 ;

hence m . (x * y) = (m . x) * (m . y) ; :: thesis: verum

end;m . (x * y) = 1. H by FUNCOP_1:7

.= (1. H) * (1. H)

.= (m . x) * (1. H) by FUNCOP_1:7

.= (m . x) * (m . y) by FUNCOP_1:7 ;

hence m . (x * y) = (m . x) * (m . y) ; :: thesis: verum

thus m . (1_ G) = 1_ H by FUNCOP_1:7; :: according to GROUP_1:def 13 :: thesis: verum