let R be Ring; 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; 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; 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; for s being Element of S st r = s holds
Ext_eval (f,r) = Ext_eval (f,s)
let s be Element of S; ( r = s implies Ext_eval (f,r) = Ext_eval (f,s) )
assume A1:
r = s
; 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 for n being Nat st n in dom F holds
F . n = G . nlet n be
Nat;
( n in dom F implies F . n = G . n )assume A8:
n in dom F
;
F . n = G . nA9:
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
;
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; verum