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: f is multiplicative Function of G,G

proof

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:35
.= (f . a) * b by FUNCT_1:35
.= (f . a) * (f . b) by FUNCT_1:35 ;
hence f . (a * b) = (f . a) * (f . b) ; :: thesis: verum

end;

hence f is multiplicative Function of G,G by GROUP_6:def 7; :: thesis: verum

end;

f is unity-preserving Function of G,G

proof

f . (1_ G) = 1_ G by FUNCT_1:35;
hence f is unity-preserving Function of G,G by GROUP_1:def 17; :: thesis: verum

end;

hence id the carrier of G is Homomorphism of G,G by A1; :: thesis: verum