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)

proof

let a, b be Element of G; :: thesis: f . (a * b) = (f . a) * (f . b)
f . (a * b) = a * b by FUNCT_1:18
.= (f . a) * b by FUNCT_1:18
.= (f . a) * (f . b) by FUNCT_1:18 ;
hence f . (a * b) = (f . a) * (f . b) ; :: thesis: verum

end;

f . (1_ G) = 1_ G by FUNCT_1:18;
hence id the carrier of G is Homomorphism of G,G by A1, GROUP_1:def 13, GROUP_6:def 6; :: thesis: verum