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 RAdj (F,T) = 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 RAdj (F,T) = 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 RAdj (F,T) = Image_hom_Ext_eval (x,F)
let x be T -evaluating Function of (card T),E; :: thesis: RAdj (F,T) = 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;
A: T is Subset of the carrier of (Image_hom_Ext_eval (x,F)) by lemphi4ab;
B: F is Subring of Image_hom_Ext_eval (x,F) by lemphi3;
( Image_hom_Ext_eval (x,F) is Subring of RAdj (F,T) & RAdj (F,T) is Subring of E ) by lemphi4aa;
then Image_hom_Ext_eval (x,F) is Subring of E by lemring;
then C: RAdj (F,T) is Subring of Image_hom_Ext_eval (x,F) by A, B, FIELD_6:32;
Image_hom_Ext_eval (x,F) is Subring of RAdj (F,T) by lemphi4aa;
hence RAdj (F,T) = Image_hom_Ext_eval (x,F) by C, FIELD_6:12; :: thesis: verum