let G be Group; :: thesis: for a, b being Element of G holds (a ") |^ b = (a |^ b) "
let a, b be Element of G; :: thesis: (a ") |^ b = (a |^ b) "
thus (a ") |^ b = ((a * b) ") * b by GROUP_1:17
.= ((a * b) ") * ((b ") ")
.= ((b ") * (a * b)) " by GROUP_1:17
.= (a |^ b) " by GROUP_1:def 3 ; :: thesis: verum