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 "
|.(- 1).| = - (- 1) by ABSVALUE:def 1;
hence h |^ (- 1) = (h |^ 1) " by Def8
.= h " by Th25 ;
:: thesis: verum