let R be Ring; :: thesis: for S being RingExtension of R
for a being Element of S
for p being Polynomial of R holds Ext_eval ((- p),a) = - (Ext_eval (p,a))
let S be RingExtension of R; :: thesis: for a being Element of S
for p being Polynomial of R holds Ext_eval ((- p),a) = - (Ext_eval (p,a))
let a be Element of S; :: thesis: for p being Polynomial of R holds Ext_eval ((- p),a) = - (Ext_eval (p,a))
let p be Polynomial of R; :: thesis: Ext_eval ((- p),a) = - (Ext_eval (p,a))
consider G being FinSequence of S such that
A: ( Ext_eval (p,a) = Sum G & len G = len p & ( for n being Element of NAT st n in dom G holds
G . n = (In ((p . (n -' 1)),S)) * ((power S) . (a,(n -' 1))) ) ) by ALGNUM_1:def 1;
consider H being FinSequence of S such that
B: ( Ext_eval ((- p),a) = Sum H & len H = len (- p) & ( for n being Element of NAT st n in dom H holds
H . n = (In (((- p) . (n -' 1)),S)) * ((power S) . (a,(n -' 1))) ) ) by ALGNUM_1:def 1;
K: R is Subring of S by FIELD_4:def 1;
then H: the carrier of R c= the carrier of S by C0SP1:def 3;
C: len G = len H by A, B, POLYNOM4:8;

now :: thesis: for n being Nat
for b being Element of S st n in dom H & b = G . n holds
H . n = - b

let n be Nat; :: thesis: for b being Element of S st n in dom H & b = G . n holds
H . n = - b
let b be Element of S; :: thesis: ( n in dom H & b = G . n implies H . n = - b )
assume D1: ( n in dom H & b = G . n ) ; :: thesis: H . n = - b
D2: dom H = Seg (len G) by C, FINSEQ_1:def 3
.= dom G by FINSEQ_1:def 3 ;
reconsider pn1 = p . (n -' 1), mpn1 = - (p . (n -' 1)) as Element of S by H;
thus H . n = (In (((- p) . (n -' 1)),S)) * ((power S) . (a,(n -' 1))) by B, D1
.= (In ((- (p . (n -' 1))),S)) * ((power S) . (a,(n -' 1))) by BHSP_1:44
.= mpn1 * ((power S) . (a,(n -' 1)))
.= (- pn1) * ((power S) . (a,(n -' 1))) by K, Th19
.= - ((In ((p . (n -' 1)),S)) * ((power S) . (a,(n -' 1)))) by VECTSP_1:9
.= - b by D1, D2, A ; :: thesis: verum

end;

hence Ext_eval ((- p),a) = - (Ext_eval (p,a)) by A, B, POLYNOM4:8, RLVECT_1:40; :: thesis: verum