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

(Conjugate (1_ G)) . q = q ;

thus Conjugate (1_ G) = id the carrier of G by A1; :: thesis: verum

for a being Element of G holds (Conjugate (1_ G)) . a = a

proof

then A1:
for q being object st q in the carrier of G holds
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;a |^ (1_ G) = a by GROUP_3:19;

hence (Conjugate (1_ G)) . a = a by Def6; :: thesis: verum

(Conjugate (1_ G)) . q = q ;

thus Conjugate (1_ G) = id the carrier of G by A1; :: thesis: verum