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