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