for F being Field
for E being FieldExtension of F
for a being Element of E
for n being Element of NAT
for M being Subset of (VecSp (E,F)) st M = { (a |^ i) where i is Element of NAT : i <= n } & ( for i, j being Element of NAT st i < j & j <= n holds
a |^ i <> a |^ j ) holds
for l being Linear_Combination of M
for p being Polynomial of F st deg p <= n & ( for i being Element of NAT st i <= n holds
p . i = l . (a |^ i) ) holds
Ext_eval (p,a) = Sum l