theorem lembasx2: :: FIELD_6:47

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