let R, T be Ring; :: thesis: for S being Subring of R
for f being Polynomial of S
for g being Polynomial of R st f = g holds
for a being Element of R holds Ext_eval (f,(In (a,T))) = Ext_eval (g,(In (a,T)))
let S be Subring of R; :: thesis: for f being Polynomial of S
for g being Polynomial of R st f = g holds
for a being Element of R holds Ext_eval (f,(In (a,T))) = Ext_eval (g,(In (a,T)))
let f be Polynomial of S; :: thesis: for g being Polynomial of R st f = g holds
for a being Element of R holds Ext_eval (f,(In (a,T))) = Ext_eval (g,(In (a,T)))
let g be Polynomial of R; :: thesis: ( f = g implies for a being Element of R holds Ext_eval (f,(In (a,T))) = Ext_eval (g,(In (a,T))) )
assume A1: f = g ; :: thesis: for a being Element of R holds Ext_eval (f,(In (a,T))) = Ext_eval (g,(In (a,T)))
let a be Element of R; :: thesis: Ext_eval (f,(In (a,T))) = Ext_eval (g,(In (a,T)))
consider F being FinSequence of T such that
A2: Ext_eval (f,(In (a,T))) = Sum F and
A3: len F = len f and
A4: for n being Element of NAT st n in dom F holds
F . n = (In ((f . (n -' 1)),T)) * ((power T) . ((In (a,T)),(n -' 1))) by ALGNUM_1:def 1;
consider G being FinSequence of T such that
A5: Ext_eval (g,(In (a,T))) = Sum G and
A6: len G = len g and
A7: for n being Element of NAT st n in dom G holds
G . n = (In ((g . (n -' 1)),T)) * ((power T) . ((In (a,T)),(n -' 1))) by ALGNUM_1:def 1;
consider Z being sequence of T such that
A8: Sum G = Z . (len G) and
A9: Z . 0 = 0. T and
A10: for j being Nat
for v being Element of T st j < len G & v = G . (j + 1) holds
Z . (j + 1) = (Z . j) + v by RLVECT_1:def 12;
A11: Sum G = Z . (len F) by A1, A3, A6, A8, Th9;

now :: thesis: for j being Nat
for v being Element of T st j < len F & v = F . (j + 1) holds
Z . (j + 1) = (Z . j) + v

let j be Nat; :: thesis: for v being Element of T st j < len F & v = F . (j + 1) holds
Z . (j + 1) = (Z . j) + v
let v be Element of T; :: thesis: ( j < len F & v = F . (j + 1) implies Z . (j + 1) = (Z . j) + v )
assume that
A12: j < len F and
A13: v = F . (j + 1) ; :: thesis: Z . (j + 1) = (Z . j) + v
A14: len F = len G by A1, A3, A6, Th9;
A15: dom F = dom G by A1, A3, A6, Th9, FINSEQ_3:29;
j + 1 <= len F by A12, NAT_1:13;
then A16: j + 1 in dom F by NAT_1:11, FINSEQ_3:25;
then F . (j + 1) = (In ((f . ((j + 1) -' 1)),T)) * ((power T) . ((In (a,T)),((j + 1) -' 1))) by A4
.= G . (j + 1) by A1, A7, A15, A16 ;
hence Z . (j + 1) = (Z . j) + v by A10, A12, A13, A14; :: thesis: verum

end;

hence Ext_eval (f,(In (a,T))) = Ext_eval (g,(In (a,T))) by A2, A5, A9, A11, RLVECT_1:def 12; :: thesis: verum