let F be Field; :: thesis: for p being Element of the carrier of (Polynom-Ring F)
for E being FieldExtension of F
for q being Element of the carrier of (Polynom-Ring E) st q = p holds
for U being b₂ -extending FieldExtension of F
for a being Element of U holds Ext_eval (q,a) = Ext_eval (p,a)
let p be Element of the carrier of (Polynom-Ring F); :: thesis: for E being FieldExtension of F
for q being Element of the carrier of (Polynom-Ring E) st q = p holds
for U being b₁ -extending FieldExtension of F
for a being Element of U holds Ext_eval (q,a) = Ext_eval (p,a)
let E be FieldExtension of F; :: thesis: for q being Element of the carrier of (Polynom-Ring E) st q = p holds
for U being E -extending FieldExtension of F
for a being Element of U holds Ext_eval (q,a) = Ext_eval (p,a)
let q be Element of the carrier of (Polynom-Ring E); :: thesis: ( q = p implies for U being E -extending FieldExtension of F
for a being Element of U holds Ext_eval (q,a) = Ext_eval (p,a) )
assume AS1: q = p ; :: thesis: for U being E -extending FieldExtension of F
for a being Element of U holds Ext_eval (q,a) = Ext_eval (p,a)
let U be E -extending FieldExtension of F; :: thesis: for a being Element of U holds Ext_eval (q,a) = Ext_eval (p,a)
let a be Element of U; :: thesis: Ext_eval (q,a) = Ext_eval (p,a)
consider Fp being FinSequence of U 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)),U)) * ((power U) . (a,(n -' 1))) ) ) by ALGNUM_1:def 1;
consider Fq being FinSequence of U such that
B: ( Ext_eval (q,a) = Sum Fq & len Fq = len q & ( for n being Element of NAT st n in dom Fq holds
Fq . n = (In ((q . (n -' 1)),U)) * ((power U) . (a,(n -' 1))) ) ) by ALGNUM_1:def 1;
C: (len p) - 1 = deg p by HURWITZ:def 2
.= deg q by AS1, FIELD_4:20
.= (len q) - 1 by HURWITZ:def 2 ;
D: dom Fp = Seg (len Fq) by A, B, C, FINSEQ_1:def 3
.= dom Fq by FINSEQ_1:def 3 ;

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
hence Fq . n = (In ((p . (n -' 1)),U)) * ((power U) . (a,(n -' 1))) by B, AS1
.= Fp . n by A, D, F ;
:: thesis: verum

end;

then Fp = Fq by D;
hence Ext_eval (q,a) = Ext_eval (p,a) by A, B; :: thesis: verum