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

A1: now :: thesis: ((j - 1) * h) + (h + ((- j) * h)) = 0_ G

per cases ( j >= 1 or j < 0 or j = 0 ) by Lm13;

suppose A2: j >= 1 ; :: thesis: ((j - 1) * h) + (h + ((- j) * h)) = 0_ G

then A3: j >= 1 + 0 ;
A4: |.(j - 1).| + 1 = (j - 1) + 1 by A3, XREAL_1:19, ABSVALUE:def 1
.= j ;
A5: |.j.| = j by A2, ABSVALUE:def 1;
A6: |.j.| = |.(- j).| by COMPLEX1:52;
thus ((j - 1) * h) + (h + ((- j) * h)) = (((j - 1) * h) + h) + ((- j) * h) by RLVECT_1:def 3
.= ((|.(j - 1).| * h) + h) + ((- j) * h) by A3, Def8, XREAL_1:19
.= ((|.(j - 1).| * h) + h) + (- (|.(- j).| * h)) by A2, Th29
.= ((|.(j - 1).| + 1) * h) + (- (|.(- j).| * h)) by Lm6
.= 0_ G by A4, A5, A6, Def5 ; :: thesis: verum

end;

suppose A7: j < 0 ; :: thesis: ((j - 1) * h) + (h + ((- j) * h)) = 0_ G

A8: 1 - j = - (j - 1) ;
thus ((j - 1) * h) + (h + ((- j) * h)) = (- (|.(j - 1).| * h)) + (h + ((- j) * h)) by A7, Def8
.= (- (|.(j - 1).| * h)) + (h + (|.(- j).| * h)) by A7, Def8
.= (- (|.(j - 1).| * h)) + ((1 + |.(- j).|) * h) by Lm6
.= (- (|.(j - 1).| * h)) + ((1 + (- j)) * h) by A7, ABSVALUE:def 1
.= (- (|.(j - 1).| * h)) + (|.(j - 1).| * h) by A7, A8, ABSVALUE:def 1
.= 0_ G by Def5 ; :: thesis: verum

end;

suppose A9: j = 0 ; :: thesis: ((j - 1) * h) + (h + ((- j) * h)) = 0_ G

hence ((j - 1) * h) + (h + ((- j) * h)) = (- h) + (h + ((- j) * h)) by Th31
.= ((- h) + h) + ((- j) * h) by RLVECT_1:def 3
.= (0_ G) + ((- j) * h) by Def5
.= 0 * h by A9, Def4
.= 0_ G by Def7 ;
:: thesis: verum

end;

end;

end;

((j - 1) * h) + ((1 - j) * h) = ((j - 1) * h) + ((- (j - 1)) * h)
.= ((j - 1) * h) + (- ((j - 1) * h)) by Lm12
.= 0_ G by Def5 ;
then h + ((- j) * h) = (1 - j) * h by A1, Th6;
then - ((1 - j) * h) = (- ((- j) * h)) + (- h) by Th16
.= ((- (- j)) * h) + (- h) by Lm12
.= (j * h) + ((- 1) * h) by Th31 ;
then (j * h) + ((- 1) * h) = (- (1 - j)) * h by Lm12;
hence (j - 1) * h = (j * h) + ((- 1) * h) ; :: thesis: verum