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