let G be Group; for a, b being Element of G holds [.a,b,a.] = [.(a |^ b),a.]
let a, b be Element of G; [.a,b,a.] = [.(a |^ b),a.]
thus [.a,b,a.] =
(([.b,a.] * (a ")) * [.a,b.]) * a
by Th22
.=
(((a ") |^ b) * ((((a ") * (b ")) * a) * b)) * a
by GROUP_3:1
.=
(((a |^ b) ") * ((((a ") * (b ")) * a) * b)) * a
by GROUP_3:26
.=
(((a |^ b) ") * (((a ") * (b ")) * (a * b))) * a
by GROUP_1:def 3
.=
(((a |^ b) ") * ((a ") * ((b ") * (a * b)))) * a
by GROUP_1:def 3
.=
(((a |^ b) ") * ((a ") * (a |^ b))) * a
by GROUP_1:def 3
.=
[.(a |^ b),a.]
by Th16
; verum