let G be 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:25 ;
hence ((Conjugate a) * (Conjugate (a "))) . b = b by FUNCT_2:15; :: 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 Th23 ; :: thesis: verum

end;

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