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: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