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 = (b ") * (((((a ") * ((b ") ")) * a) * (b ")) * b) by GROUP_1:def 3
.= (b ") * ((((a ") * ((b ") ")) * a) * ((b ") * b)) by GROUP_1:def 3
.= (b ") * ((((a ") * ((b ") ")) * a) * (1_ G)) by GROUP_1:def 5
.= (b ") * (((a ") * ((b ") ")) * a) by GROUP_1:def 4
.= (b ") * ((a ") * (b * a)) by GROUP_1:def 3
.= ((b ") * (a ")) * (b * a) by GROUP_1:def 3
.= (((b ") * (a ")) * b) * a by GROUP_1:def 3
.= [.b,a.] ; :: thesis: verum