let i be Integer; :: thesis: for G being addGroup
for h being Element of G st i <= 0 holds
i * h = - (|.i.| * h)
let G be addGroup; :: thesis: for h being Element of G st i <= 0 holds
i * h = - (|.i.| * h)
let h be Element of G; :: thesis: ( i <= 0 implies i * h = - (|.i.| * h) )
assume A1: i <= 0 ; :: thesis: i * h = - (|.i.| * h)

per cases ( i < 0 or i = 0 ) by A1;

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

hence i * h = - (|.i.| * h) by Def8; :: thesis: verum

end;

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

hence i * h = 0_ G by Lm3
.= - (0_ G) by Th8
.= - (0 * h) by Def7
.= - (|.i.| * h) by A2, ABSVALUE:def 1 ;
:: thesis: verum

end;

end;