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