theorem lembas2: :: FIELD_6:64

for F being Field
for E being FieldExtension of F
for a being b₁ -algebraic Element of E
for l being Linear_Combination of Base a st Sum l = 0. F holds
l = ZeroLC (VecSp ((FAdj (F,{a})),F))