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;