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