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) + (((- 1) * h) + ((- j) * h)) = 0_ G

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

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

then reconsider n = j as Element of NAT by INT_1:3;
A3: n + 1 = |.(j + 1).| by ABSVALUE:def 1;
n + 1 >= 0 ;
hence ((j + 1) * h) + (((- 1) * h) + ((- j) * h)) = (|.(j + 1).| * h) + (((- 1) * h) + ((- j) * h)) by Def8
.= (|.(j + 1).| * h) + ((- h) + ((- j) * h)) by Th31
.= (|.(j + 1).| * h) + ((- h) + (- (j * h))) by Lm12
.= (|.(j + 1).| * h) + ((- h) + (- (|.j.| * h))) by A2, Def8
.= (|.(j + 1).| * h) + (- ((|.j.| * h) + h)) by Th16
.= (|.(j + 1).| * h) + (- ((|.j.| + 1) * h)) by Lm6
.= (|.(j + 1).| * h) + (- (|.(j + 1).| * h)) by A3, ABSVALUE:def 1
.= 0_ G by Def5 ;
:: thesis: verum

end;

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

then A4: j + 1 < (- 1) + 1 by XREAL_1:6;
hence ((j + 1) * h) + (((- 1) * h) + ((- j) * h)) = (- (|.(j + 1).| * h)) + (((- 1) * h) + ((- j) * h)) by Def8
.= (- (|.(j + 1).| * h)) + ((- h) + ((- j) * h)) by Th31
.= ((- (|.(j + 1).| * h)) + (- h)) + ((- j) * h) by RLVECT_1:def 3
.= (- (h + (|.(j + 1).| * h))) + ((- j) * h) by Th16
.= (- ((|.(j + 1).| + 1) * h)) + ((- j) * h) by Lm6
.= (- (((- (j + 1)) + 1) * h)) + ((- j) * h) by A4, ABSVALUE:def 1
.= 0_ G by Def5 ;
:: thesis: verum

end;

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

hence ((j + 1) * h) + (((- 1) * h) + ((- j) * h)) = (0_ G) + (((- 1) * h) + ((- j) * h)) by Lm3
.= ((- 1) * h) + ((- j) * h) by Def4
.= (- h) + ((- j) * h) by Th31
.= (- h) + (- (j * h)) by Lm12
.= (- h) + (- (- h)) by A5, Th31
.= 0_ G by Def5 ;
:: thesis: verum

end;

end;

end;

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