let G be non empty well-unital multLoopStr ; :: thesis: id the carrier of G is Homomorphism of G,G

reconsider f = id the carrier of G as Function of G,G ;

A1: for a, b being Element of G holds f . (a * b) = (f . a) * (f . b) ;

f . (1_ G) = 1_ G ;

hence id the carrier of G is Homomorphism of G,G by A1, GROUP_1:def 13, GROUP_6:def 6; :: thesis: verum

reconsider f = id the carrier of G as Function of G,G ;

A1: for a, b being Element of G holds f . (a * b) = (f . a) * (f . b) ;

f . (1_ G) = 1_ G ;

hence id the carrier of G is Homomorphism of G,G by A1, GROUP_1:def 13, GROUP_6:def 6; :: thesis: verum