let L be non empty right_complementable Abelian add-associative right_zeroed distributive unital doubleLoopStr ; :: thesis: for p being Polynomial of L
for x being Element of L holds eval ((- p),x) = - (eval (p,x))
let p be Polynomial of L; :: thesis: for x being Element of L holds eval ((- p),x) = - (eval (p,x))
let x be Element of L; :: thesis: eval ((- p),x) = - (eval (p,x))
consider F1 being FinSequence of the carrier of L such that
A1: eval (p,x) = Sum F1 and
A2: len F1 = len p and
A3: for n being Element of NAT st n in dom F1 holds
F1 . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) by Def2;
consider F2 being FinSequence of the carrier of L such that
A4: eval ((- p),x) = Sum F2 and
A5: len F2 = len (- p) and
A6: for n being Element of NAT st n in dom F2 holds
F2 . n = ((- p) . (n -' 1)) * ((power L) . (x,(n -' 1))) by Def2;
len F2 = len F1 by A2, A5, Th8;
then A7: dom F2 = dom F1 by FINSEQ_3:29;

now :: thesis: for n being Nat
for v being Element of L st n in dom F2 & v = F1 . n holds
F2 . n = - v

let n be Nat; :: thesis: for v being Element of L st n in dom F2 & v = F1 . n holds
F2 . n = - v
let v be Element of L; :: thesis: ( n in dom F2 & v = F1 . n implies F2 . n = - v )
assume that
A8: n in dom F2 and
A9: v = F1 . n ; :: thesis: F2 . n = - v
thus F2 . n = ((- p) . (n -' 1)) * ((power L) . (x,(n -' 1))) by A6, A8
.= (- (p . (n -' 1))) * ((power L) . (x,(n -' 1))) by BHSP_1:44
.= - ((p . (n -' 1)) * ((power L) . (x,(n -' 1)))) by VECTSP_1:9
.= - v by A3, A7, A8, A9 ; :: thesis: verum

end;

hence eval ((- p),x) = - (eval (p,x)) by A1, A2, A4, A5, Th8, RLVECT_1:40; :: thesis: verum