let G be addGroup; :: thesis: for h being Element of G holds (- 1) * h = - h
let h be Element of G; :: thesis: (- 1) * h = - h
|.(- 1).| = - (- 1) by ABSVALUE:def 1;
hence (- 1) * h = - (1 * h) by Def8
.= - h by Th25 ;
:: thesis: verum