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 3
.= (((a ") * [.b,(a ").]) * [.b,a.]) * a by Th19
.= ([.b,(a ").] * [.b,a.]) |^ a by GROUP_1:def 3 ; :: thesis: verum