let F be Field; :: thesis: for E being FieldExtension of F
for T being non empty finite Subset of E
for p being Polynomial of (card T),F st ex b being bag of card T st Support p = {b} holds
for x being b₂ -evaluating Function of (card T),E holds Ext_eval (p,x) in the carrier of (RAdj (F,T))
let E be FieldExtension of F; :: thesis: for T being non empty finite Subset of E
for p being Polynomial of (card T),F st ex b being bag of card T st Support p = {b} holds
for x being b₁ -evaluating Function of (card T),E holds Ext_eval (p,x) in the carrier of (RAdj (F,T))
let T be non empty finite Subset of E; :: thesis: for p being Polynomial of (card T),F st ex b being bag of card T st Support p = {b} holds
for x being T -evaluating Function of (card T),E holds Ext_eval (p,x) in the carrier of (RAdj (F,T))
let p be Polynomial of (card T),F; :: thesis: ( ex b being bag of card T st Support p = {b} implies for x being T -evaluating Function of (card T),E holds Ext_eval (p,x) in the carrier of (RAdj (F,T)) )
assume AS: ex b being bag of card T st Support p = {b} ; :: thesis: for x being T -evaluating Function of (card T),E holds Ext_eval (p,x) in the carrier of (RAdj (F,T))
let x be T -evaluating Function of (card T),E; :: thesis: Ext_eval (p,x) in the carrier of (RAdj (F,T))
set n = card T;
A0: F is Subring of E by FIELD_4:def 1;
consider y being FinSequence of the carrier of E such that
A2: ( Ext_eval (p,x) = Sum y & len y = len (SgmX ((BagOrder (card T)),(Support p))) & ( for i being Element of NAT st 1 <= i & i <= len y holds
y . i = (In (((p * (SgmX ((BagOrder (card T)),(Support p)))) . i),E)) * (eval (((SgmX ((BagOrder (card T)),(Support p))) /. i),x)) ) ) by FIELD_11:def 4;
A3: len (SgmX ((BagOrder (card T)),(Support p))) = card (Support p) by PRE_POLY:11, POLYNOM2:18
.= 1 by AS, CARD_2:42 ;
then H: 1 in Seg (len y) by A2, FINSEQ_1:1;
then 1 in dom y by FINSEQ_1:def 3;
then A5: y . 1 = y /. 1 by PARTFUN1:def 6;
F is Subring of RAdj (F,T) by FIELD_6:31;
then A8: the carrier of F c= the carrier of (RAdj (F,T)) by C0SP1:def 3;
dom (SgmX ((BagOrder (card T)),(Support p))) = Seg (len y) by A2, FINSEQ_1:def 3
.= dom y by FINSEQ_1:def 3 ;
then A9: 1 in dom (SgmX ((BagOrder (card T)),(Support p))) by H, FINSEQ_1:def 3;
dom p = Bags (card T) by FUNCT_2:def 1;
then (SgmX ((BagOrder (card T)),(Support p))) /. 1 in dom p ;
then (SgmX ((BagOrder (card T)),(Support p))) . 1 in dom p by A9, PARTFUN1:def 6;
then p . ((SgmX ((BagOrder (card T)),(Support p))) . 1) in rng p by FUNCT_1:3;
then A4: (p * (SgmX ((BagOrder (card T)),(Support p)))) . 1 in rng p by A9, FUNCT_1:13;
A7: rng p c= the carrier of F by RELAT_1:def 19;
the carrier of F c= the carrier of E by A0, C0SP1:def 3;
then A6: In (((p * (SgmX ((BagOrder (card T)),(Support p)))) . 1),E) = (p * (SgmX ((BagOrder (card T)),(Support p)))) . 1 by A4, A7, SUBSET_1:def 8;
reconsider c = (p * (SgmX ((BagOrder (card T)),(Support p)))) . 1 as Element of (RAdj (F,T)) by A4, A7, A8;
reconsider a = eval (((SgmX ((BagOrder (card T)),(Support p))) /. 1),x) as Element of (RAdj (F,T)) by lemphi2a;
y = <*(y . 1)*> by A2, A3, FINSEQ_1:40;
then Ext_eval (p,x) = y /. 1 by A2, A5, RLVECT_1:44
.= (In (((p * (SgmX ((BagOrder (card T)),(Support p)))) . 1),E)) * (eval (((SgmX ((BagOrder (card T)),(Support p))) /. 1),x)) by A5, A3, A2
.= c * a by A6, FIELD_6:16 ;
hence Ext_eval (p,x) in the carrier of (RAdj (F,T)) ; :: thesis: verum