theorem u1: :: FIELD_8:46

for F being Field
for E being FieldExtension of F
for a being b₁ -algebraic Element of E holds
( 0. (FAdj (F,{a})) = Ext_eval ((0_. F),a) & 1. (FAdj (F,{a})) = Ext_eval ((1_. F),a) )