theorem lembas2bb: :: FIELD_6:62

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
for p being non zero Polynomial of F st l . (a |^ (deg p)) = LC p & Carrier l = {(a |^ (deg p))} holds
Sum l = Ext_eval ((LM p),a)