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