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