let R be Ring; :: thesis: for S being Subring of R
for f being Polynomial of S
for r being Element of R
for s being Element of S st r = s holds
Ext_eval (f,r) = Ext_eval (f,s)
let S be Subring of R; :: thesis: for f being Polynomial of S
for r being Element of R
for s being Element of S st r = s holds
Ext_eval (f,r) = Ext_eval (f,s)
let f be Polynomial of S; :: thesis: for r being Element of R
for s being Element of S st r = s holds
Ext_eval (f,r) = Ext_eval (f,s)
let r be Element of R; :: thesis: for s being Element of S st r = s holds
Ext_eval (f,r) = Ext_eval (f,s)
let s be Element of S; :: thesis: ( r = s implies Ext_eval (f,r) = Ext_eval (f,s) )
assume A1: r = s ; :: thesis: Ext_eval (f,r) = Ext_eval (f,s)
consider F being FinSequence of R such that
A2: Ext_eval (f,r) = 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)),R)) * ((power R) . (r,(n -' 1))) by ALGNUM_1:def 1;
consider G being FinSequence of S such that
A5: Ext_eval (f,s) = Sum G and
A6: len G = len f and
A7: for n being Element of NAT st n in dom G holds
G . n = (In ((f . (n -' 1)),S)) * ((power S) . (s,(n -' 1))) by ALGNUM_1:def 1;

now :: thesis: for n being Nat st n in dom F holds
F . n = G . n

let n be Nat; :: thesis: ( n in dom F implies F . n = G . n )
assume A8: n in dom F ; :: thesis: F . n = G . n
A9: dom F = dom G by A3, A6, FINSEQ_3:29;
A10: r = In (s,R) by A1;
A11: (f . (n -' 1)) * ((power S) . (s,(n -' 1))) is Element of R by Th7;
thus F . n = (In ((f . (n -' 1)),R)) * ((power R) . (r,(n -' 1))) by A4, A8
.= In (((f . (n -' 1)) * ((power S) . (s,(n -' 1)))),R) by A10, ALGNUM_1:11
.= (In ((f . (n -' 1)),S)) * ((power S) . (s,(n -' 1))) by A11
.= G . n by A7, A8, A9 ; :: thesis: verum

end;

then F = G by A3, A6, FINSEQ_2:9;
then A12: In ((Sum G),R) = Sum F by ALGNUM_1:10;
Sum G is Element of R by Th7;
hence Ext_eval (f,r) = Ext_eval (f,s) by A2, A5, A12; :: thesis: verum