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