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