let R, T be Ring; :: thesis:
let S be Subring of R; :: thesis:
let f be Polynomial of S; :: thesis:
let g be Polynomial of R; :: thesis:
assume A1: f = g ; :: thesis:
let a be Element of R; :: thesis:
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;

let j be Nat; :: thesis:
let v be Element of T; :: thesis:
assume that
A12: j < len F and
A13: v = F . (j + 1) ; :: thesis:
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:

end;