let G be Group; :: thesis: for a being Element of G holds
( a |^ (a " ) = a & (a " ) |^ a = a " )
let a be Element of G; :: thesis: ( a |^ (a " ) = a & (a " ) |^ a = a " )
thus a |^ (a " ) = (a * a) * (a " ) by GROUP_1:19
.= a by Th1 ; :: thesis: (a " ) |^ a = a "
thus (a " ) |^ a = a " by Th1; :: thesis: verum