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

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