let G be Group; :: thesis: for a, b being Element of G holds [.a,b,a.] = [.(a |^ b),a.]
let a, b be Element of G; :: thesis: [.a,b,a.] = [.(a |^ b),a.]
thus [.a,b,a.] = (([.b,a.] * (a ")) * [.a,b.]) * a by Th25
.= (((a ") |^ b) * ((((a ") * (b ")) * a) * b)) * a by GROUP_3:1
.= (((a |^ b) ") * ((((a ") * (b ")) * a) * b)) * a by GROUP_3:32
.= (((a |^ b) ") * (((a ") * (b ")) * (a * b))) * a by GROUP_1:def 4
.= (((a |^ b) ") * ((a ") * ((b ") * (a * b)))) * a by GROUP_1:def 4
.= (((a |^ b) ") * ((a ") * (a |^ b))) * a by GROUP_1:def 4
.= [.(a |^ b),a.] by Th19 ; :: thesis: verum