theorem exteval2: :: FIELD_14:26

for F being Field
for a, b being Element of F
for E being FieldExtension of F
for x being Element of E holds Ext_eval (<%a,b%>,x) = (@ (a,E)) + ((@ (b,E)) * x)