theorem eval0: :: FIELD_11:37

for F being Field
for E being FieldExtension of F
for m being Ordinal st m in card (nonConstantPolys F) holds
for p being Polynomial of F
for x being Function of (card (nonConstantPolys F)),E holds Ext_eval ((Poly (m,p)),x) = Ext_eval (p,(x /. m))