let R be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; for a being Element of R
for i being Element of NAT holds - ((Nat-mult-left R) . (i,a)) = (Nat-mult-left R) . (i,(- a))
let a be Element of R; for i being Element of NAT holds - ((Nat-mult-left R) . (i,a)) = (Nat-mult-left R) . (i,(- a))
let i be Element of NAT ; - ((Nat-mult-left R) . (i,a)) = (Nat-mult-left R) . (i,(- a))
defpred S1[ Nat] means ((Nat-mult-left R) . ($1,a)) + ((Nat-mult-left R) . ($1,(- a))) = 0. R;
A1:
S1[ 0 ]
A2:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A3:
S1[
n]
;
S1[n + 1]
((Nat-mult-left R) . ((n + 1),a)) + ((Nat-mult-left R) . ((n + 1),(- a))) =
(a + ((Nat-mult-left R) . (n,a))) + ((Nat-mult-left R) . ((n + 1),(- a)))
by BINOM:def 3
.=
(a + ((Nat-mult-left R) . (n,a))) + ((- a) + ((Nat-mult-left R) . (n,(- a))))
by BINOM:def 3
.=
((a + ((Nat-mult-left R) . (n,a))) + ((Nat-mult-left R) . (n,(- a)))) + (- a)
by RLVECT_1:def 3
.=
(a + (((Nat-mult-left R) . (n,a)) + ((Nat-mult-left R) . (n,(- a))))) + (- a)
by RLVECT_1:def 3
.=
a + (- a)
by A3, RLVECT_1:4
.=
0. R
by RLVECT_1:5
;
hence
S1[
n + 1]
;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A2);
then
((Nat-mult-left R) . (i,a)) + ((Nat-mult-left R) . (i,(- a))) = 0. R
;
hence
- ((Nat-mult-left R) . (i,a)) = (Nat-mult-left R) . (i,(- a))
by RLVECT_1:6; verum