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