theorem help2m: :: FIELD_13:39

for F being Field
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 the carrier of (RAdj (F,T)) = { (Ext_eval (p,x)) where p is Polynomial of (card T),F : verum }