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;
hence eval ((- p),x) = - (eval (p,x)) by A1, A2, A4, A5, Th8, RLVECT_1:40; :: thesis: verum