theorem lembas: :: FIELD_6:65

for F being Field
for E being Polynom-Ring b₁ -homomorphic FieldExtension of F
for a being b₁ -algebraic Element of E holds Base a is Basis of (VecSp ((FAdj (F,{a})),F))