let i be Integer; :: thesis: for G being addGroup
for h being Element of G holds (- i) * h = - (i * h)
let G be addGroup; :: thesis: for h being Element of G holds (- i) * h = - (i * h)
let h be Element of G; :: thesis: (- i) * h = - (i * h)

per cases ( i >= 0 or i < 0 ) ;

suppose A1: i >= 0 ; :: thesis: (- i) * h = - (i * h)

per cases ( - i < - 0 or i = 0 ) by A1, XREAL_1:24;

suppose A2: - i < - 0 ; :: thesis: (- i) * h = - (i * h)

hence (- i) * h = - (|.(- i).| * h) by Def8
.= - ((- (- i)) * h) by A2, ABSVALUE:def 1
.= - (i * h) ;
:: thesis: verum

end;

suppose A3: i = 0 ; :: thesis: (- i) * h = - (i * h)

hence (- i) * h = 0_ G by Lm3
.= - (0_ G) by Th8
.= - (i * h) by A3, Lm3 ;
:: thesis: verum

end;

end;

end;

suppose A4: i < 0 ; :: thesis: (- i) * h = - (i * h)

then i * h = - (|.i.| * h) by Def8;
hence (- i) * h = - (i * h) by A4, ABSVALUE:def 1; :: thesis: verum

end;

end;