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