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