let G be Group; :: thesis: id the carrier of G is Homomorphism of G,G
reconsider f = id the carrier of G as Function of G,G ;

now

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

end;

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