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:26

.= (((a ") |^ (b ")) * ((b ") * ((((b ") ") * a) * (b ")))) * b by GROUP_1:def 3

.= (((a ") |^ (b ")) * ((b ") * (((b ") ") * (a * (b "))))) * b by GROUP_1:def 3

.= (((a ") |^ (b ")) * (a * (b "))) * b by GROUP_3:1

.= ((a ") |^ (b ")) * ((a * (b ")) * b) by GROUP_1:def 3

.= [.(b "),a.] by GROUP_3:1 ; :: thesis: verum

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:26

.= (((a ") |^ (b ")) * ((b ") * ((((b ") ") * a) * (b ")))) * b by GROUP_1:def 3

.= (((a ") |^ (b ")) * ((b ") * (((b ") ") * (a * (b "))))) * b by GROUP_1:def 3

.= (((a ") |^ (b ")) * (a * (b "))) * b by GROUP_3:1

.= ((a ") |^ (b ")) * ((a * (b ")) * b) by GROUP_1:def 3

.= [.(b "),a.] by GROUP_3:1 ; :: thesis: verum