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 rng (hom_Ext_eval (x,F)) c= the carrier of (RAdj (F,T))
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 rng (hom_Ext_eval (x,F)) c= the carrier of (RAdj (F,T))
let T be non empty finite Subset of E; :: thesis: for x being T -evaluating Function of (card T),E holds rng (hom_Ext_eval (x,F)) c= the carrier of (RAdj (F,T))
let x be T -evaluating Function of (card T),E; :: thesis: rng (hom_Ext_eval (x,F)) c= the carrier of (RAdj (F,T))

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

let o be object ; :: thesis: ( o in rng (hom_Ext_eval (x,F)) implies o in the carrier of (RAdj (F,T)) )
assume A: o in rng (hom_Ext_eval (x,F)) ; :: thesis: o in the carrier of (RAdj (F,T))
rng (hom_Ext_eval (x,F)) = { (Ext_eval (p,x)) where p is Polynomial of (card T),F : verum } by lemphi1;
then consider p being Polynomial of (card T),F such that
B: o = Ext_eval (p,x) by A;
thus o in the carrier of (RAdj (F,T)) by B, lemphi2b; :: thesis: verum

end;

hence rng (hom_Ext_eval (x,F)) c= the carrier of (RAdj (F,T)) ; :: thesis: verum