let n be Nat; :: thesis: for F being Field
for E being FieldExtension of F
for p being Polynomial of n,F
for q being Polynomial of n,E
for x being Function of n,E st p = q holds
Ext_eval (p,x) = eval (q,x)
let R be Field; :: thesis: for E being FieldExtension of R
for p being Polynomial of n,R
for q being Polynomial of n,E
for x being Function of n,E st p = q holds
Ext_eval (p,x) = eval (q,x)
let S be FieldExtension of R; :: thesis: for p being Polynomial of n,R
for q being Polynomial of n,S
for x being Function of n,S st p = q holds
Ext_eval (p,x) = eval (q,x)
let p be Polynomial of n,R; :: thesis: for q being Polynomial of n,S
for x being Function of n,S st p = q holds
Ext_eval (p,x) = eval (q,x)
let q be Polynomial of n,S; :: thesis: for x being Function of n,S st p = q holds
Ext_eval (p,x) = eval (q,x)
let x be Function of n,S; :: thesis: ( p = q implies Ext_eval (p,x) = eval (q,x) )
assume A1: p = q ; :: thesis: Ext_eval (p,x) = eval (q,x)
R is Subring of S by FIELD_4:def 1;
then A2: the carrier of R c= the carrier of S by C0SP1:def 3;
consider Fp being FinSequence of the carrier of S such that
A6: ( Ext_eval (p,x) = Sum Fp & len Fp = len (SgmX ((BagOrder n),(Support p))) & ( for i being Element of NAT st 1 <= i & i <= len Fp holds
Fp . i = (In (((p * (SgmX ((BagOrder n),(Support p)))) . i),S)) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) ) ) by FIELD_11:def 4;
consider Fq being FinSequence of the carrier of S such that
A7: ( len Fq = len (SgmX ((BagOrder n),(Support q))) & eval (q,x) = Sum Fq & ( for i being Element of NAT st 1 <= i & i <= len Fq holds
Fq /. i = ((q * (SgmX ((BagOrder n),(Support q)))) /. i) * (eval (((SgmX ((BagOrder n),(Support q))) /. i),x)) ) ) by POLYNOM2:def 4;
A11: dom Fq = Seg (len (SgmX ((BagOrder n),(Support q)))) by A7, FINSEQ_1:def 3
.= Seg (len (SgmX ((BagOrder n),(Support p)))) by A1, field426a
.= dom Fp by A6, FINSEQ_1:def 3 ;
for i being Nat st i in dom Fp holds
Fq . i = Fp . i

proof

let i be Nat; :: thesis: ( i in dom Fp implies Fq . i = Fp . i )
assume A12: i in dom Fp ; :: thesis: Fq . i = Fp . i
then ( i in Seg (len Fp) & i in Seg (len Fq) ) by A11, FINSEQ_1:def 3;
then A13: ( 1 <= i & i <= len Fp & i <= len Fq ) by FINSEQ_1:1;
A14: i is Element of NAT by ORDINAL1:def 12;
A15: eval (((SgmX ((BagOrder n),(Support p))) /. i),x) = eval (((SgmX ((BagOrder n),(Support q))) /. i),x) by A1, field426a;
A19: dom Fq = Seg (len (SgmX ((BagOrder n),(Support q)))) by A7, FINSEQ_1:def 3
.= dom (SgmX ((BagOrder n),(Support q))) by FINSEQ_1:def 3 ;
then A18: ( i in dom (SgmX ((BagOrder n),(Support q))) & i in dom (SgmX ((BagOrder n),(Support p))) ) by A11, A12, A1, field426a;
dom q = Bags n by FUNCT_2:def 1;
then (SgmX ((BagOrder n),(Support q))) /. i in dom q ;
then A17: i in dom (q * (SgmX ((BagOrder n),(Support q)))) by A19, A11, A12, PARTFUN2:3;
dom p = Bags n by FUNCT_2:def 1;
then (SgmX ((BagOrder n),(Support p))) /. i in dom p ;
then (SgmX ((BagOrder n),(Support p))) . i in dom p by A18, PARTFUN1:def 6;
then p . ((SgmX ((BagOrder n),(Support p))) . i) in rng p by FUNCT_1:3;
then A20: (p * (SgmX ((BagOrder n),(Support p)))) . i in rng p by A18, FUNCT_1:13;
A21: rng p c= the carrier of R by RELAT_1:def 19;
A16: In (((p * (SgmX ((BagOrder n),(Support p)))) . i),S) = (p * (SgmX ((BagOrder n),(Support p)))) . i by A20, A21, A2, SUBSET_1:def 8
.= (q * (SgmX ((BagOrder n),(Support q)))) . i by A1, field426a
.= (q * (SgmX ((BagOrder n),(Support q)))) /. i by A17, PARTFUN1:def 6 ;
thus Fp . i = (In (((p * (SgmX ((BagOrder n),(Support p)))) . i),S)) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) by A6, A13, A14
.= Fq /. i by A7, A13, A14, A15, A16
.= Fq . i by A11, A12, PARTFUN1:def 6 ; :: thesis: verum

end;

hence Ext_eval (p,x) = eval (q,x) by A6, A7, A11, FINSEQ_1:13; :: thesis: verum