let G be strict Group; :: thesis: for a being Element of G holds (Conjugate a) * (Conjugate (a " )) = Conjugate (1_ G)
let a be Element of G; :: thesis: (Conjugate a) * (Conjugate (a " )) = Conjugate (1_ G)
set f1 = (Conjugate a) * (Conjugate (a " ));
set f2 = Conjugate (1_ G);
A1: for b being Element of G holds ((Conjugate a) * (Conjugate (a " ))) . b = b

proof

let b be Element of G; :: thesis: ((Conjugate a) * (Conjugate (a " ))) . b = b
(Conjugate a) . ((Conjugate (a " )) . b) = (Conjugate a) . (b |^ (a " )) by Def6
.= (b |^ (a " )) |^ a by Def6
.= b by GROUP_3:30 ;
hence ((Conjugate a) * (Conjugate (a " ))) . b = b by FUNCT_2:21; :: thesis: verum

end;

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

proof

let b be Element of G; :: thesis: ((Conjugate a) * (Conjugate (a " ))) . b = (Conjugate (1_ G)) . b
thus ((Conjugate a) * (Conjugate (a " ))) . b = b by A1
.= (Conjugate (1_ G)) . b by Th25 ; :: thesis: verum

end;

hence (Conjugate a) * (Conjugate (a " )) = Conjugate (1_ G) by FUNCT_2:113; :: thesis: verum