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