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) = Conjugate (1_ G) by Th25
.= id the carrier of G by Th22 ;
A2: Conjugate a is Element of Aut G by Th12;
then Conjugate a is Homomorphism of G,G by Def1;
then A3: Conjugate a is one-to-one by A2, Def1;
rng (Conjugate a) = dom (Conjugate a) by A2, Lm3
.= the carrier of G by A2, Lm3 ;
hence Conjugate (a ") = (Conjugate a) " by A1, A3, FUNCT_2:30; :: thesis: verum