let G be Group; :: thesis: for a, b being Element of G holds Conjugate (a * b) = (Conjugate b) * (Conjugate a)
let a, b be Element of G; :: thesis: Conjugate (a * b) = (Conjugate b) * (Conjugate a)
set f1 = Conjugate (a * b);
set f2 = (Conjugate b) * (Conjugate a);
A1: for c being Element of G holds (Conjugate (a * b)) . c = (c |^ a) |^ b

proof

let c be Element of G; :: thesis: (Conjugate (a * b)) . c = (c |^ a) |^ b
c |^ (a * b) = (c |^ a) |^ b by GROUP_3:24;
hence (Conjugate (a * b)) . c = (c |^ a) |^ b by Def6; :: thesis: verum

end;

A2: for c being Element of G holds (Conjugate (a * b)) . c = (Conjugate b) . (c |^ a)

proof

let c be Element of G; :: thesis: (Conjugate (a * b)) . c = (Conjugate b) . (c |^ a)
(c |^ a) |^ b = (Conjugate b) . (c |^ a) by Def6;
hence (Conjugate (a * b)) . c = (Conjugate b) . (c |^ a) by A1; :: thesis: verum

end;

A3: for c being Element of G holds (Conjugate (a * b)) . c = (Conjugate b) . ((Conjugate a) . c)

proof

let c be Element of G; :: thesis: (Conjugate (a * b)) . c = (Conjugate b) . ((Conjugate a) . c)
(Conjugate b) . (c |^ a) = (Conjugate b) . ((Conjugate a) . c) by Def6;
hence (Conjugate (a * b)) . c = (Conjugate b) . ((Conjugate a) . c) by A2; :: thesis: verum

end;

for c being Element of G holds (Conjugate (a * b)) . c = ((Conjugate b) * (Conjugate a)) . c

proof

let c be Element of G; :: thesis: (Conjugate (a * b)) . c = ((Conjugate b) * (Conjugate a)) . c
(Conjugate b) . ((Conjugate a) . c) = ((Conjugate b) * (Conjugate a)) . c by FUNCT_2:15;
hence (Conjugate (a * b)) . c = ((Conjugate b) * (Conjugate a)) . c by A3; :: thesis: verum

end;

hence Conjugate (a * b) = (Conjugate b) * (Conjugate a) ; :: thesis: verum