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 4; :: thesis: verum