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