let G be Group; :: thesis: for a, b being Element of G holds [.a,b.] " = [.b,a.]

let a, b be Element of G; :: thesis: [.a,b.] " = [.b,a.]

thus [.a,b.] " = (((a ") * (b ")) * (a * b)) " by Th16

.= ((a * b) ") * (((a ") * (b ")) ") by GROUP_1:17

.= ((b ") * (a ")) * (((a ") * (b ")) ") by GROUP_1:17

.= ((b ") * (a ")) * (((b ") ") * ((a ") ")) by GROUP_1:17

.= ((b ") * (a ")) * (((b ") ") * a)

.= ((b ") * (a ")) * (b * a)

.= [.b,a.] by Th16 ; :: thesis: verum

let a, b be Element of G; :: thesis: [.a,b.] " = [.b,a.]

thus [.a,b.] " = (((a ") * (b ")) * (a * b)) " by Th16

.= ((a * b) ") * (((a ") * (b ")) ") by GROUP_1:17

.= ((b ") * (a ")) * (((a ") * (b ")) ") by GROUP_1:17

.= ((b ") * (a ")) * (((b ") ") * ((a ") ")) by GROUP_1:17

.= ((b ") * (a ")) * (((b ") ") * a)

.= ((b ") * (a ")) * (b * a)

.= [.b,a.] by Th16 ; :: thesis: verum