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 '*' (j '*' a)
let a be Element of R; :: thesis: for i, j being Integer holds (i * j) '*' a = i '*' (j '*' a)
let i, j be Integer; :: thesis: (i * j) '*' a = i '*' (j '*' a)
defpred S1[ Integer] means for k being Integer st k = $1 holds
(k * j) '*' a = k '*' (j '*' a);
now :: thesis: for k being Integer st k = 0 holds
(k * j) '*' a = k '*' (j '*' a)
let k be Integer; :: thesis: ( k = 0 implies (k * j) '*' a = k '*' (j '*' a) )
assume A1: k = 0 ; :: thesis: (k * j) '*' a = k '*' (j '*' a)
hence (k * j) '*' a = 0. R by Th58
.= k '*' (j '*' a) by A1, Th58 ;
:: thesis: verum
end;
then A2: S1[ 0 ] ;
A3: for u being Integer st S1[u] holds
( S1[u - 1] & S1[u + 1] )
proof
let u be Integer; :: thesis: ( S1[u] implies ( S1[u - 1] & S1[u + 1] ) )
assume A4: S1[u] ; :: thesis: ( S1[u - 1] & S1[u + 1] )
now :: thesis: for k being Integer st k = u - 1 holds
(k * j) '*' a = k '*' (j '*' a)
let k be Integer; :: thesis: ( k = u - 1 implies (k * j) '*' a = k '*' (j '*' a) )
assume A5: k = u - 1 ; :: thesis: (k * j) '*' a = k '*' (j '*' a)
hence (k * j) '*' a = ((u * j) - j) '*' a
.= ((u * j) '*' a) - (j '*' a) by Th63
.= (u '*' (j '*' a)) - (j '*' a) by A4
.= k '*' (j '*' a) by A5, Lm6 ;
:: thesis: verum
end;
hence S1[u - 1] ; :: thesis: S1[u + 1]
now :: thesis: for k being Integer st k = u + 1 holds
(k * j) '*' a = k '*' (j '*' a)
let k be Integer; :: thesis: ( k = u + 1 implies (k * j) '*' a = k '*' (j '*' a) )
assume A6: k = u + 1 ; :: thesis: (k * j) '*' a = k '*' (j '*' a)
hence (k * j) '*' a = ((u * j) + j) '*' a
.= ((u * j) '*' a) + (j '*' a) by Th61
.= (u '*' (j '*' a)) + (j '*' a) by A4
.= k '*' (j '*' a) by A6, Lm5 ;
:: thesis: verum
end;
hence S1[u + 1] ; :: thesis: verum
end;
for i being Integer holds S1[i] from INT_1:sch 4(A2, A3);
 hence (i * j) '*' a = i '*' (j '*' a) ; :: thesis: verum