let R be non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for a being Element of R
for i being Integer holds (i + 1) '*' a = (i '*' a) + a
let a be Element of R; :: thesis: for i being Integer holds (i + 1) '*' a = (i '*' a) + a
let i be Integer; :: thesis: (i + 1) '*' a = (i '*' a) + a
i in INT by INT_1:def 2;
then consider n being Nat such that
A1: ( i = n or i = - n ) by INT_1:def 1;

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

suppose A2: n = 0 ; :: thesis: (i + 1) '*' a = (i '*' a) + a

hence (i + 1) '*' a = (0. R) + a by A1, Th59
.= (i '*' a) + a by A1, A2, Th58 ;
:: thesis: verum

end;

suppose A3: n <> 0 ; :: thesis: (i + 1) '*' a = (i '*' a) + a

per cases ( i = n or i = - n ) by A1;

suppose A4: i = n ; :: thesis: (i + 1) '*' a = (i '*' a) + a

then A5: i '*' a = n * a by Def2;
(n + 1) * a = (n * a) + (1 * a) by BINOM:15
.= (n * a) + a by BINOM:13 ;
hence (i + 1) '*' a = (i '*' a) + a by A4, A5, Def2; :: thesis: verum

end;

suppose A6: i = - n ; :: thesis: (i + 1) '*' a = (i '*' a) + a

reconsider n1 = n - 1 as Element of NAT by INT_1:3, A3;
(n1 + 1) * a = (n1 * a) + (1 * a) by BINOM:15
.= (n1 * a) + a by BINOM:13 ;
then i '*' a = - ((n1 * a) + a) by A6, Def2
.= (- (n1 * a)) + (- a) by RLVECT_1:31 ;
then A7: (i '*' a) + a = (- (n1 * a)) + ((- a) + a) by RLVECT_1:def 3
.= (- (n1 * a)) + (0. R) by RLVECT_1:5 ;
i + 1 = - (n - 1) by A6;
hence (i + 1) '*' a = (i '*' a) + a by Def2, A7; :: thesis: verum

end;

end;

end;

end;