theorem lembasx1a: :: FIELD_6:48

for F being Field
for E being FieldExtension of F
for a being Element of E
for n being Element of NAT
for l being Linear_Combination of VecSp (E,F)
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)