let R, T be Ring; 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; 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; 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; ( 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
; 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; 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 for j being Nat
for v being Element of T st j < len F & v = F . (j + 1) holds
Z . (j + 1) = (Z . j) + vlet j be
Nat;
for v being Element of T st j < len F & v = F . (j + 1) holds
Z . (j + 1) = (Z . j) + vlet v be
Element of
T;
( 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)
;
Z . (j + 1) = (Z . j) + vA14:
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;
verum end;
hence
Ext_eval (f,(In (a,T))) = Ext_eval (g,(In (a,T)))
by A2, A5, A9, A11, RLVECT_1:def 12; verum