let G be strict Group; :: thesis: for a being Element of G holds Conjugate (a " ) = (Conjugate a) "
let a be Element of G; :: thesis: Conjugate (a " ) = (Conjugate a) "
set f = Conjugate a;
set g = Conjugate (a " );
A1: (Conjugate (a " )) * (Conjugate a) = id the carrier of G

proof

thus (Conjugate (a " )) * (Conjugate a) = Conjugate (1_ G) by Th27
.= id the carrier of G by Th24 ; :: thesis: verum

end;

A2: Conjugate a is Element of Aut G by Th13;
then A3: rng (Conjugate a) = dom (Conjugate a) by Lm3
.= the carrier of G by A2, Lm3 ;
Conjugate a is Homomorphism of G,G by A2, Def1;
then Conjugate a is one-to-one by A2, Def1;
hence Conjugate (a " ) = (Conjugate a) " by A1, A3, FUNCT_2:36; :: thesis: verum