theorem help3: :: FIELD_13:48

for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for h being b₁ -fixing Monomorphism of E,K
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 h . (Ext_eval (p,x)) in the carrier of (RAdj (F,(h .: T)))