let R be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: 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; :: thesis: 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 ; :: thesis: - ((Nat-mult-left R) . (i,a)) = (Nat-mult-left R) . (i,(- a))
defpred S₁[ Nat] means ((Nat-mult-left R) . ($1,a)) + ((Nat-mult-left R) . ($1,(- a))) = 0. R;
A1: S₁[ 0 ]

proof

((Nat-mult-left R) . (0,a)) + ((Nat-mult-left R) . (0,(- a))) = (0. R) + ((Nat-mult-left R) . (0,(- a))) by BINOM:def 3
.= (0. R) + (0. R) by BINOM:def 3
.= 0. R by RLVECT_1:4 ;
hence S₁[ 0 ] ; :: thesis: verum

end;

A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[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 S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[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; :: thesis: verum