let G be Group; :: thesis: for h being Element of G holds h |^ (- 1) = h "
let h be Element of G; :: thesis: h |^ (- 1) = h "
( abs (- 1) = - (- 1) & - (- 1) = 1 ) by ABSVALUE:def 1;
hence h |^ (- 1) = (h |^ 1) " by Def9
.= h " by Th44 ;
:: thesis: verum