let R be non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for a being Element of R
for i, j being Integer holds (i + j) '*' a = (i '*' a) + (j '*' a)
let a be Element of R; :: thesis: for i, j being Integer holds (i + j) '*' a = (i '*' a) + (j '*' a)
let i, j be Integer; :: thesis: (i + j) '*' a = (i '*' a) + (j '*' a)
defpred S₁[ Integer] means for k being Integer st k = $1 holds
(i + k) '*' a = (i '*' a) + (k '*' a);

now :: thesis: for k being Integer st k = 0 holds
(i + k) '*' a = (i '*' a) + (k '*' a)

let k be Integer; :: thesis: ( k = 0 implies (i + k) '*' a = (i '*' a) + (k '*' a) )
assume A1: k = 0 ; :: thesis: (i + k) '*' a = (i '*' a) + (k '*' a)
hence (i + k) '*' a = (i '*' a) + (0. R)
.= (i '*' a) + (k '*' a) by A1, Th58 ;
:: thesis: verum

end;

then A2: S₁[ 0 ] ;
A3: for u being Integer st S₁[u] holds
( S₁[u - 1] & S₁[u + 1] )

proof

let u be Integer; :: thesis: ( S₁[u] implies ( S₁[u - 1] & S₁[u + 1] ) )
assume A4: S₁[u] ; :: thesis: ( S₁[u - 1] & S₁[u + 1] )

now :: thesis: for k being Integer st k = u - 1 holds
(i + k) '*' a = (i '*' a) + (k '*' a)

let k be Integer; :: thesis: ( k = u - 1 implies (i + k) '*' a = (i '*' a) + (k '*' a) )
assume k = u - 1 ; :: thesis: (i + k) '*' a = (i '*' a) + (k '*' a)
then A5: (i + (k + 1)) '*' a = (i '*' a) + ((k + 1) '*' a) by A4
.= (i '*' a) + ((k '*' a) + a) by Lm5
.= ((i '*' a) + (k '*' a)) + a by RLVECT_1:def 3 ;
(i + (k + 1)) '*' a = ((i + k) + 1) '*' a
.= ((i + k) '*' a) + a by Lm5 ;
hence (i + k) '*' a = (i '*' a) + (k '*' a) by A5, RLVECT_1:8; :: thesis: verum

end;

hence S₁[u - 1] ; :: thesis: S₁[u + 1]

now :: thesis: for k being Integer st k = u + 1 holds
(i + k) '*' a = (i '*' a) + (k '*' a)

let k be Integer; :: thesis: ( k = u + 1 implies (i + k) '*' a = (i '*' a) + (k '*' a) )
assume k = u + 1 ; :: thesis: (i + k) '*' a = (i '*' a) + (k '*' a)
then A6: (i + (k - 1)) '*' a = (i '*' a) + ((k - 1) '*' a) by A4
.= (i '*' a) + ((k '*' a) - a) by Lm6
.= ((i '*' a) + (k '*' a)) - a by RLVECT_1:def 3 ;
(i + (k - 1)) '*' a = ((i + k) - 1) '*' a
.= ((i + k) '*' a) - a by Lm6 ;
hence (i + k) '*' a = (i '*' a) + (k '*' a) by A6, RLVECT_1:8; :: thesis: verum

end;

hence S₁[u + 1] ; :: thesis: verum

end;

for i being Integer holds S₁[i] from INT_1:sch 4(A2, A3);
hence (i + j) '*' a = (i '*' a) + (j '*' a) ; :: thesis: verum