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 Th60, A1
.= (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 i - 1 = - (n + 1) ;
hence (i - 1) '*' a = - ((n + 1) * a) by Def2
.= - ((n * a) + (1 * a)) by BINOM:15
.= - ((n * a) + a) by BINOM:13
.= (- (n * a)) + (- a) by RLVECT_1:31
.= (i '*' a) - a by A4, Def2 ;
:: thesis: verum

end;

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

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

end;

end;

end;

end;