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

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

for b being Element of G holds ((Conjugate (a ")) * (Conjugate a)) . b = (Conjugate (1_ G)) . b
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;(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

proof

hence
(Conjugate (a ")) * (Conjugate a) = Conjugate (1_ G)
; :: thesis: verum
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;thus ((Conjugate (a ")) * (Conjugate a)) . b = b by A1

.= (Conjugate (1_ G)) . b by Th23 ; :: thesis: verum