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 b being bag of card T st ex o being set st support b = {o} holds
for x being b₄ -evaluating Function of (card T),E holds h . (eval (b,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 b being bag of card T st ex o being set st support b = {o} holds
for x being b₃ -evaluating Function of (card T),E holds h . (eval (b,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 b being bag of card T st ex o being set st support b = {o} holds
for x being b₂ -evaluating Function of (card T),E holds h . (eval (b,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 b being bag of card T st ex o being set st support b = {o} holds
for x being b₁ -evaluating Function of (card T),E holds h . (eval (b,x)) in the carrier of (RAdj (F,(h .: T)))
let T be non empty finite Subset of E; :: thesis: for b being bag of card T st ex o being set st support b = {o} holds
for x being T -evaluating Function of (card T),E holds h . (eval (b,x)) in the carrier of (RAdj (F,(h .: T)))
let b be bag of card T; :: thesis: ( ex o being set st support b = {o} implies for x being T -evaluating Function of (card T),E holds h . (eval (b,x)) in the carrier of (RAdj (F,(h .: T))) )
assume AS: ex o being set st support b = {o} ; :: thesis: for x being T -evaluating Function of (card T),E holds h . (eval (b,x)) in the carrier of (RAdj (F,(h .: T)))
let x be T -evaluating Function of (card T),E; :: thesis: h . (eval (b,x)) in the carrier of (RAdj (F,(h .: T)))
consider o being set such that
A: support b = {o} by AS;
o in {o} by TARSKI:def 1;
then reconsider o = o as Element of card T by A;
B: h .: T is Subset of (RAdj (F,(h .: T))) by FIELD_6:30;
C: rng x c= T by RELAT_1:def 19;
D: ( o in support b & support b c= dom b ) by A, TARSKI:def 1, PRE_POLY:37;
dom b = card T by PARTFUN1:def 2
.= dom x by FUNCT_2:def 1 ;
then E: x . o in T by C, D, FUNCT_1:3;
dom h = the carrier of E by FUNCT_2:def 1;
then h . (x . o) in h .: T by E, FUNCT_1:def 6;
then reconsider a = h . (x . o) as Element of (RAdj (F,(h .: T))) by B;
reconsider c = x . o as Element of E ;
h . (eval (b,x)) = h . ((power E) . ((x . o),(b . o))) by A, POLYNOM2:15
.= h . (c |^ (b . o)) by BINOM:def 2
.= (h . c) |^ (b . o) by FIELD_1:13
.= a |^ (b . o) by FIELD_6:19
.= (power (RAdj (F,(h .: T)))) . (a,(b . o)) by BINOM:def 2 ;
hence h . (eval (b,x)) in the carrier of (RAdj (F,(h .: T))) ; :: thesis: verum