theorem lemphi2b: :: FIELD_13:37

for F being Field
for E being FieldExtension of F
for T being non empty finite Subset of E
for p being Polynomial of (card T),F
for x being b₃ -evaluating Function of (card T),E holds Ext_eval (p,x) in the carrier of (RAdj (F,T))