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