let G be Group; :: thesis: Conjugate (1_ G) = id the carrier of G
for a being Element of G holds (Conjugate (1_ G)) . a = a

proof

let a be Element of G; :: thesis: (Conjugate (1_ G)) . a = a
a |^ (1_ G) = a by GROUP_3:19;
hence (Conjugate (1_ G)) . a = a by Def6; :: thesis: verum

end;

then for q being object st q in the carrier of G holds
(Conjugate (1_ G)) . q = q ;
hence Conjugate (1_ G) = id the carrier of G ; :: thesis: verum