let F be Field; :: thesis: for E being FieldExtension of F
for K being F -extending FieldExtension of F
for h being F -fixing Monomorphism of E,K
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 h . (Ext_eval (p,x)) in the carrier of (RAdj (F,(h .: T)))
let E be FieldExtension of F; :: thesis: for K being F -extending FieldExtension of F
for h being F -fixing Monomorphism of E,K
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 h . (Ext_eval (p,x)) in the carrier of (RAdj (F,(h .: T)))
let K be F -extending FieldExtension of F; :: thesis: for h being F -fixing Monomorphism of E,K
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 h . (Ext_eval (p,x)) in the carrier of (RAdj (F,(h .: T)))
let h be F -fixing Monomorphism of E,K; :: 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 h . (Ext_eval (p,x)) in the carrier of (RAdj (F,(h .: 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 h . (Ext_eval (p,x)) in the carrier of (RAdj (F,(h .: 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 h . (Ext_eval (p,x)) in the carrier of (RAdj (F,(h .: 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 h . (Ext_eval (p,x)) in the carrier of (RAdj (F,(h .: T)))
let x be T -evaluating Function of (card T),E; :: thesis: h . (Ext_eval (p,x)) in the carrier of (RAdj (F,(h .: 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;
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 U: (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;
A6: the carrier of F c= the carrier of E by A0, C0SP1:def 3;
set b = (SgmX ((BagOrder (card T)),(Support p))) /. 1;
reconsider a = h . (eval (((SgmX ((BagOrder (card T)),(Support p))) /. 1),x)) as Element of (RAdj (F,(h .: T))) by Lm9;
F is Subring of RAdj (F,(h .: T)) by FIELD_6:31;
then Y: the carrier of F c= the carrier of (RAdj (F,(h .: T))) by C0SP1:def 3;
Z: 1 in dom (p * (SgmX ((BagOrder (card T)),(Support p)))) by U, A9, FUNCT_1:11;
h . (In (((p * (SgmX ((BagOrder (card T)),(Support p)))) . 1),E)) = h . ((p * (SgmX ((BagOrder (card T)),(Support p)))) . 1) by A4, A6, A7, SUBSET_1:def 8
.= h . ((p * (SgmX ((BagOrder (card T)),(Support p)))) /. 1) by Z, PARTFUN1:def 6
.= (p * (SgmX ((BagOrder (card T)),(Support p)))) /. 1 by FIELD_8:def 2 ;
then reconsider c = h . (In (((p * (SgmX ((BagOrder (card T)),(Support p)))) . 1),E)) as Element of (RAdj (F,(h .: T))) by Y;
y = <*(y . 1)*> by A2, A3, FINSEQ_1:40;
then h . (Ext_eval (p,x)) = h . (y /. 1) by A2, A5, RLVECT_1:44
.= h . ((In (((p * (SgmX ((BagOrder (card T)),(Support p)))) . 1),E)) * (eval (((SgmX ((BagOrder (card T)),(Support p))) /. 1),x))) by A5, A3, A2
.= (h . (In (((p * (SgmX ((BagOrder (card T)),(Support p)))) . 1),E))) * (h . (eval (((SgmX ((BagOrder (card T)),(Support p))) /. 1),x))) by GROUP_6:def 6
.= c * a by FIELD_6:16 ;
hence h . (Ext_eval (p,x)) in the carrier of (RAdj (F,(h .: T))) ; :: thesis: verum