let F be Field; :: thesis: for E being FieldExtension of F
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 eval (b,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 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 eval (b,x) in the carrier of (RAdj (F,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 eval (b,x) in the carrier of (RAdj (F,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 eval (b,x) in the carrier of (RAdj (F,T)) )
assume AS: ex o being set st support b = {o} ; :: thesis: for x being T -evaluating Function of (card T),E holds eval (b,x) in the carrier of (RAdj (F,T))
let x be T -evaluating Function of (card T),E; :: thesis: eval (b,x) in the carrier of (RAdj (F,T))
consider o being set such that
A: support b = {o} by AS;
B: T is Subset of (RAdj (F,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 x . o in T by C, D, FUNCT_1:3;
then reconsider a = x . o as Element of (RAdj (F,T)) by B;
reconsider c = x . o as Element of E by D, FUNCT_2:5;
eval (b,x) = (power E) . ((x . o),(b . o)) by A, POLYNOM2:15
.= c |^ (b . o) by BINOM:def 2
.= a |^ (b . o) by FIELD_6:19
.= (power (RAdj (F,T))) . (a,(b . o)) by BINOM:def 2 ;
hence eval (b,x) in the carrier of (RAdj (F,T)) ; :: thesis: verum