let F be Field; :: thesis: for p being Element of the carrier of (Polynom-Ring F)
for E being FieldExtension of F
for K being b₂ -extending FieldExtension of F
for a being Element of E
for b being Element of K st a = b holds
Ext_eval (p,a) = Ext_eval (p,b)
let p be Element of the carrier of (Polynom-Ring F); :: thesis: for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for a being Element of E
for b being Element of K st a = b holds
Ext_eval (p,a) = Ext_eval (p,b)
let E be FieldExtension of F; :: thesis: for K being E -extending FieldExtension of F
for a being Element of E
for b being Element of K st a = b holds
Ext_eval (p,a) = Ext_eval (p,b)
let U be E -extending FieldExtension of F; :: thesis: for a being Element of E
for b being Element of U st a = b holds
Ext_eval (p,a) = Ext_eval (p,b)
let a be Element of E; :: thesis: for b being Element of U st a = b holds
Ext_eval (p,a) = Ext_eval (p,b)
let b be Element of U; :: thesis: ( a = b implies Ext_eval (p,a) = Ext_eval (p,b) )
assume AS2: a = b ; :: thesis: Ext_eval (p,a) = Ext_eval (p,b)
H1: E is Subring of U by FIELD_4:def 1;
then H2: the carrier of E c= the carrier of U by C0SP1:def 3;
F is Subring of E by FIELD_4:def 1;
then H4: the carrier of F c= the carrier of E by C0SP1:def 3;
consider Fp being FinSequence of E such that
A: ( Ext_eval (p,a) = Sum Fp & len Fp = len p & ( for n being Element of NAT st n in dom Fp holds
Fp . n = (In ((p . (n -' 1)),E)) * ((power E) . (a,(n -' 1))) ) ) by ALGNUM_1:def 1;
consider Fq being FinSequence of U such that
B: ( Ext_eval (p,b) = Sum Fq & len Fq = len p & ( for n being Element of NAT st n in dom Fq holds
Fq . n = (In ((p . (n -' 1)),U)) * ((power U) . (b,(n -' 1))) ) ) by ALGNUM_1:def 1;

C: now :: thesis: for n being Element of NAT holds (power U) . (b,(n -' 1)) = (power E) . (a,(n -' 1))

let n be Element of NAT ; :: thesis: (power U) . (b,(n -' 1)) = (power E) . (a,(n -' 1))
thus (power U) . (b,(n -' 1)) = (power U) . ((In (b,U)),(n -' 1))
.= In (((power E) . (a,(n -' 1))),U) by AS2, H1, ALGNUM_1:7
.= (power E) . (a,(n -' 1)) by H2, SUBSET_1:def 8 ; :: thesis: verum

end;

D: dom Fp = Seg (len Fq) by A, B, FINSEQ_1:def 3
.= dom Fq by FINSEQ_1:def 3 ;

E: now :: thesis: for n being Element of NAT holds In ((p . (n -' 1)),U) = In ((p . (n -' 1)),E)

let n be Element of NAT ; :: thesis: In ((p . (n -' 1)),U) = In ((p . (n -' 1)),E)
p . (n -' 1) in U by H2, H4;
hence In ((p . (n -' 1)),U) = p . (n -' 1) by SUBSET_1:def 8
.= In ((p . (n -' 1)),E) by H4, SUBSET_1:def 8 ;
:: thesis: verum

end;

H: for n being Element of NAT holds [(In ((p . (n -' 1)),E)),((power E) . (a,(n -' 1)))] in [: the carrier of E, the carrier of E:] by ZFMISC_1:def 2;

now :: thesis: for n being Nat st n in dom Fq holds
Fq . n = Fp . n

let n be Nat; :: thesis: ( n in dom Fq implies Fq . n = Fp . n )
assume F: n in dom Fq ; :: thesis: Fq . n = Fp . n
G: n is Element of NAT by ORDINAL1:def 12;
thus Fq . n = (In ((p . (n -' 1)),U)) * ((power U) . (b,(n -' 1))) by B, F
.= the multF of U . ((In ((p . (n -' 1)),U)),((power E) . (a,(n -' 1)))) by C, G
.= the multF of U . ((In ((p . (n -' 1)),E)),((power E) . (a,(n -' 1)))) by E, G
.= ( the multF of U || the carrier of E) . ((In ((p . (n -' 1)),E)),((power E) . (a,(n -' 1)))) by G, H, FUNCT_1:49
.= (In ((p . (n -' 1)),E)) * ((power E) . (a,(n -' 1))) by H1, C0SP1:def 3
.= Fp . n by A, D, F ; :: thesis: verum

end;

then Fp = Fq by D;
hence Ext_eval (p,a) = Ext_eval (p,b) by H1, A, B, FIELD_4:2; :: thesis: verum