let G be strict 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:24;
hence (Conjugate (1_ G)) . a = a by Def6; :: thesis: verum

end;

then A1: for q being set st q in the carrier of G holds
(Conjugate (1_ G)) . q = q ;
Conjugate (1_ G) is Element of Aut G by Th13;
then dom (Conjugate (1_ G)) = the carrier of G by Lm3;
hence Conjugate (1_ G) = id the carrier of G by A1, FUNCT_1:34; :: thesis: verum