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