theorem alg00: :: FIELD_6:43

for F being Field
for E being FieldExtension of F
for a being Element of E holds
( a is F -algebraic iff ex p being non zero Polynomial of F st Ext_eval (p,a) = 0. E )