let G be Group; :: thesis: for a, b being Element of G holds [.a,b.] = ((b * a) ") * (a * b)
let a, b be Element of G; :: thesis: [.a,b.] = ((b * a) ") * (a * b)
thus [.a,b.] = ((a ") * (b ")) * (a * b) by Th19
.= ((b * a) ") * (a * b) by GROUP_1:25 ; :: thesis: verum