let F be Field; 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 b2 -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); for E being FieldExtension of F
for q being Element of the carrier of (Polynom-Ring E) st q = p holds
for U being b1 -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; 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); ( 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
; 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; for a being Element of U holds Ext_eval (q,a) = Ext_eval (p,a)
let a be Element of U; 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
;
then
Fp = Fq
by D;
hence
Ext_eval (q,a) = Ext_eval (p,a)
by A, B; verum