let G be Group; :: thesis: for a, b being Element of G holds ([.a,(b ").] |^ b) " = [.(b "),a.] |^ b
let a, b be Element of G; :: thesis: ([.a,(b ").] |^ b) " = [.(b "),a.] |^ b
thus ([.a,(b ").] |^ b) " = ([.a,(b ").] ") |^ b by GROUP_3:26
.= [.(b "),a.] |^ b by GROUP_5:22 ; :: thesis: verum