let F be Field; :: thesis: for E being FieldExtension of F
for T being non empty finite Subset of E
for o being object st o in the carrier of (RAdj (F,T)) holds
ex p being Polynomial of (card T),F ex x being b₂ -evaluating Function of (card T),E st o = Ext_eval (p,x)
let E be FieldExtension of F; :: thesis: for T being non empty finite Subset of E
for o being object st o in the carrier of (RAdj (F,T)) holds
ex p being Polynomial of (card T),F ex x being b₁ -evaluating Function of (card T),E st o = Ext_eval (p,x)
let T be non empty finite Subset of E; :: thesis: for o being object st o in the carrier of (RAdj (F,T)) holds
ex p being Polynomial of (card T),F ex x being T -evaluating Function of (card T),E st o = Ext_eval (p,x)
let o be object ; :: thesis: ( o in the carrier of (RAdj (F,T)) implies ex p being Polynomial of (card T),F ex x being T -evaluating Function of (card T),E st o = Ext_eval (p,x) )
assume A: o in the carrier of (RAdj (F,T)) ; :: thesis: ex p being Polynomial of (card T),F ex x being T -evaluating Function of (card T),E st o = Ext_eval (p,x)
set x = the T -evaluating Function of (card T),E;
the carrier of (RAdj (F,T)) = { (Ext_eval (p, the T -evaluating Function of (card T),E)) where p is Polynomial of (card T),F : verum } by help2m;
then consider p being Polynomial of (card T),F such that
B: o = Ext_eval (p, the T -evaluating Function of (card T),E) by A;
thus ex p being Polynomial of (card T),F ex x being T -evaluating Function of (card T),E st o = Ext_eval (p,x) by B; :: thesis: verum