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:25
.= ((a * b) " ) * ((b " ) " )
.= ((b " ) * (a * b)) " by GROUP_1:25
.= (a |^ b) " by GROUP_1:def 4 ; :: thesis: verum