let F be Field; :: thesis: 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)
let a, b be Element of F; :: thesis: for E being FieldExtension of F
for x being Element of E holds Ext_eval (<%a,b%>,x) = (@ (a,E)) + ((@ (b,E)) * x)
let E be FieldExtension of F; :: thesis: for x being Element of E holds Ext_eval (<%a,b%>,x) = (@ (a,E)) + ((@ (b,E)) * x)
let x be Element of E; :: thesis: Ext_eval (<%a,b%>,x) = (@ (a,E)) + ((@ (b,E)) * x)
A: F is Subring of E by FIELD_4:def 1;
B: ( <%a,b%> is Element of the carrier of (Polynom-Ring F) & <%(@ (a,E)),(@ (b,E))%> is Element of the carrier of (Polynom-Ring E) ) by POLYNOM3:def 10;
( a = @ (a,E) & b = @ (b,E) ) by FIELD_7:def 4;
then <%(@ (a,E)),(@ (b,E))%> = <%a,b%> by A, FIELD_6:20;
hence Ext_eval (<%a,b%>,x) = eval (<%(@ (a,E)),(@ (b,E))%>,x) by B, FIELD_4:26
.= (@ (a,E)) + ((@ (b,E)) * x) by POLYNOM5:44 ;
:: thesis: verum