let F be Field; :: thesis: for E being FieldExtension of F
for T being non empty finite Subset of E
for x being b₂ -evaluating Function of (card T),E holds T is Subset of the carrier of (Image_hom_Ext_eval (x,F))
let E be FieldExtension of F; :: thesis: for T being non empty finite Subset of E
for x being b₁ -evaluating Function of (card T),E holds T is Subset of the carrier of (Image_hom_Ext_eval (x,F))
let T be non empty finite Subset of E; :: thesis: for x being T -evaluating Function of (card T),E holds T is Subset of the carrier of (Image_hom_Ext_eval (x,F))
let x be T -evaluating Function of (card T),E; :: thesis: T is Subset of the carrier of (Image_hom_Ext_eval (x,F))
set R = Image_hom_Ext_eval (x,F);
set S = RAdj (F,T);
set f = hom_Ext_eval (x,F);
set n = card T;

now :: thesis: for o being object st o in T holds
o in the carrier of (Image_hom_Ext_eval (x,F))

let o be object ; :: thesis: ( o in T implies o in the carrier of (Image_hom_Ext_eval (x,F)) )
assume A1: o in T ; :: thesis: o in the carrier of (Image_hom_Ext_eval (x,F))
then reconsider a = o as Element of E ;
rng x = T by tev;
then consider i being object such that
A2: ( i in dom x & x . i = a ) by A1, FUNCT_1:def 3;
reconsider i = i as Element of card T by A2;
set b = ({i},1) -bag ;
defpred S₁[ Element of Bags (card T), Element of the carrier of F] means ( ( $1 = ({i},1) -bag & $2 = 1. F ) or ( $1 <> ({i},1) -bag & $2 = 0. F ) );
A: for x being Element of Bags (card T) ex y being Element of the carrier of F st S₁[x,y]

proof

let x be Element of Bags (card T); :: thesis: ex y being Element of the carrier of F st S₁[x,y]

per cases ( x = ({i},1) -bag or x <> ({i},1) -bag ) ;

suppose x = ({i},1) -bag ; :: thesis: ex y being Element of the carrier of F st S₁[x,y]

hence ex y being Element of the carrier of F st S₁[x,y] ; :: thesis: verum

end;

suppose x <> ({i},1) -bag ; :: thesis: ex y being Element of the carrier of F st S₁[x,y]

hence ex y being Element of the carrier of F st S₁[x,y] ; :: thesis: verum

end;

end;

end;

consider p being Function of (Bags (card T)), the carrier of F such that
B: for x being Element of Bags (card T) holds S₁[x,p . x] from FUNCT_2:sch 3(A);
C: Support p = {(({i},1) -bag)}

proof

C1: now :: thesis: for o being object st o in {(({i},1) -bag)} holds
o in Support p

let o be object ; :: thesis: ( o in {(({i},1) -bag)} implies o in Support p )
assume o in {(({i},1) -bag)} ; :: thesis: o in Support p
then C2: o = ({i},1) -bag by TARSKI:def 1;
p . (({i},1) -bag) <> 0. F by B;
hence o in Support p by C2, POLYNOM1:def 4; :: thesis: verum

end;

now :: thesis: for o being object st o in Support p holds
o in {(({i},1) -bag)}

let o be object ; :: thesis: ( o in Support p implies o in {(({i},1) -bag)} )
assume C3: o in Support p ; :: thesis: o in {(({i},1) -bag)}
then reconsider b1 = o as Element of Bags (card T) ;

now :: thesis: not b1 <> ({i},1) -bag

assume b1 <> ({i},1) -bag ; :: thesis: contradiction
then p . b1 = 0. F by B;
hence contradiction by C3, POLYNOM1:def 4; :: thesis: verum

end;

hence o in {(({i},1) -bag)} by TARSKI:def 1; :: thesis: verum

end;

hence Support p = {(({i},1) -bag)} by C1, TARSKI:2; :: thesis: verum

end;

then reconsider p = p as Polynomial of (card T),F by POLYNOM1:def 5;
dom (hom_Ext_eval (x,F)) = the carrier of (Polynom-Ring ((card T),F)) by FUNCT_2:def 1;
then D: p in dom (hom_Ext_eval (x,F)) by POLYNOM1:def 11;
K: F is Subring of E by FIELD_4:def 1;
then J: the carrier of F c= the carrier of E by C0SP1:def 3;
I: 1. E = 1. F by K, C0SP1:def 3
.= In ((1. F),E) by J, SUBSET_1:def 8
.= In ((p . (({i},1) -bag)),E) by B ;
H: ( i in {i} & support (({i},1) -bag) = {i} ) by UPROOTS:8, TARSKI:def 1;
then E: eval ((({i},1) -bag),x) = (power E) . (a,((({i},1) -bag) . i)) by A2, POLYNOM2:15
.= (power E) . (a,(0 + 1)) by H, UPROOTS:7
.= ((power E) . (a,0)) * a by GROUP_1:def 7
.= (1_ E) * a by GROUP_1:def 7 ;
(hom_Ext_eval (x,F)) . p = Ext_eval (p,x) by dh
.= a by I, C, E, FIELD_11:18 ;
then a in rng (hom_Ext_eval (x,F)) by D, FUNCT_1:def 3;
hence o in the carrier of (Image_hom_Ext_eval (x,F)) by defIm; :: thesis: verum

end;

then T c= the carrier of (Image_hom_Ext_eval (x,F)) ;
hence T is Subset of the carrier of (Image_hom_Ext_eval (x,F)) ; :: thesis: verum