let L be non empty right_complementable Abelian add-associative right_zeroed unital distributive 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;
A7: len F2 = len F1 by A2, A5, Th11;
then A8: dom F2 = dom F1 by FINSEQ_3:31;

now

let n be Element of 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
A9: n in dom F2 and
A10: v = F1 . n ; :: thesis: F2 . n = - v
thus F2 . n = ((- p) . (n -' 1)) * ((power L) . x,(n -' 1)) by A6, A9
.= (- (p . (n -' 1))) * ((power L) . x,(n -' 1)) by BHSP_1:def 10
.= - ((p . (n -' 1)) * ((power L) . x,(n -' 1))) by VECTSP_1:41
.= - v by A3, A8, A9, A10 ; :: thesis: verum

end;

hence eval (- p),x = - (eval p,x) by A1, A4, A7, RLVECT_1:57; :: thesis: verum