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