let G be Group; :: thesis: for a, b being Element of G holds [.a,b.] " = [.(a "),b.] |^ a
let a, b be Element of G; :: thesis: [.a,b.] " = [.(a "),b.] |^ a
thus [.a,b.] " = (((a ") * (b ")) * (a * b)) " by GROUP_1:def 3
.= ((a * b) ") * (((a ") * (b ")) ") by GROUP_1:17
.= ((b ") * (a ")) * (((a ") * (b ")) ") by GROUP_1:17
.= ((b ") * (a ")) * (((b ") ") * ((a ") ")) by GROUP_1:17
.= (b ") * ((a ") * (b * a)) by GROUP_1:def 3
.= (b ") * (((a ") * b) * a) by GROUP_1:def 3
.= (1_ G) * ((b ") * (((a ") * b) * a)) by GROUP_1:def 4
.= ((a ") * a) * ((b ") * (((a ") * b) * a)) by GROUP_1:def 5
.= (a ") * (a * ((b ") * (((a ") * b) * a))) by GROUP_1:def 3
.= (a ") * ((a * (b ")) * (((a ") * b) * a)) by GROUP_1:def 3
.= (a ") * (((a * (b ")) * ((a ") * b)) * a) by GROUP_1:def 3
.= ((a ") * ((a * (b ")) * ((a ") * b))) * a by GROUP_1:def 3
.= [.(a "),b.] |^ a by GROUP_5:16 ; :: thesis: verum