theorem lembas2a: :: FIELD_6:61

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 ex p being Polynomial of F st
( deg p < deg (MinPoly (a,F)) & ( for i being Element of NAT st i < deg (MinPoly (a,F)) holds
p . i = l . (a |^ i) ) )