theorem u1: :: FIELD_8:46
for F being Field
for E being FieldExtension of F
for a being b1 -algebraic Element of E holds
( 0. (FAdj (F,{a})) = Ext_eval ((0_. F),a) & 1. (FAdj (F,{a})) = Ext_eval ((1_. F),a) )