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)
proof
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;
hence m is multiplicative by GROUP_6:def 6; :: thesis: m is unity-preserving
thus m . (1_ G) = 1_ H by FUNCOP_1:7; :: according to GROUP_1:def 13 :: thesis: verum