let R be non empty right_complementable Abelian add-associative right_zeroed left-distributive doubleLoopStr ; :: thesis: for a, b being Element of R
for i being Integer holds i '*' (a * b) = (i '*' a) * b
let a, b be Element of R; :: thesis: for i being Integer holds i '*' (a * b) = (i '*' a) * b
let i be Integer; :: thesis: i '*' (a * b) = (i '*' a) * b
defpred S1[ Integer] means $1 '*' (a * b) = ($1 '*' a) * b;
A2: S1[ 0 ]
proof
0 '*' a = 0. R by RING_3:59;
hence 0 '*' (a * b) = (0 '*' a) * b by RING_3:59; :: thesis: verum
end;
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] )
thus S1[u - 1] :: thesis: S1[u + 1]
proof
set k = u - 1;
A6: ((u - 1) + 1) '*' (a * b) = (((u - 1) '*' a) + (1 '*' a)) * b by A4, RING_3:62
.= (((u - 1) '*' a) * b) + ((1 '*' a) * b) by VECTSP_1:def 3
.= (((u - 1) '*' a) * b) + (a * b) by RING_3:60 ;
(((u - 1) '*' a) * b) + (0. R) = (((u - 1) '*' a) * b) + ((a * b) + (- (a * b))) by RLVECT_1:5
.= (((u - 1) + 1) '*' (a * b)) + (- (a * b)) by A6, RLVECT_1:def 3 ;
hence ((u - 1) '*' a) * b = (((u - 1) + 1) '*' (a * b)) + ((- 1) '*' (a * b)) by RING_3:61
.= (u - 1) '*' (a * b) by RING_3:62 ;
:: thesis: verum
end;
thus S1[u + 1] :: thesis: verum
proof
set k = u + 1;
A6: ((u + 1) - 1) '*' (a * b) = (((u + 1) '*' a) - (1 '*' a)) * b by A4, RING_3:64
.= (((u + 1) '*' a) * b) + ((- (1 '*' a)) * b) by VECTSP_1:def 3
.= (((u + 1) '*' a) * b) + (- ((1 '*' a) * b)) by VECTSP_1:9
.= (((u + 1) '*' a) * b) - (a * b) by RING_3:60 ;
(((u + 1) '*' a) * b) + (0. R) = (((u + 1) '*' a) * b) + ((- (a * b)) + (a * b)) by RLVECT_1:5
.= (((u + 1) - 1) '*' (a * b)) + (a * b) by A6, RLVECT_1:def 3 ;
hence ((u + 1) '*' a) * b = (((u + 1) - 1) '*' (a * b)) + (1 '*' (a * b)) by RING_3:60
.= (u + 1) '*' (a * b) by RING_3:62 ;
:: thesis: verum
end;
end;
for i being Integer holds S1[i] from INT_1:sch 4(A2, A3);
 hence i '*' (a * b) = (i '*' a) * b ; :: thesis: verum