let L be non empty right_complementable Abelian add-associative right_zeroed distributive unital doubleLoopStr ; 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; for x being Element of L holds eval ((- p),x) = - (eval (p,x))
let x be Element of L; 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;
hence
eval ((- p),x) = - (eval (p,x))
by A1, A2, A4, A5, Th8, RLVECT_1:40; verum