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