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:19;
hence (Conjugate (1_ G)) . a = a by Def6; :: thesis: verum
end;
then A1: for q being object st q in the carrier of G holds
(Conjugate (1_ G)) . q = q ;
thus Conjugate (1_ G) = id the carrier of G by A1; :: thesis: verum