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