let F be Field; :: thesis: for E being FieldExtension of F
for p being Polynomial of F st deg p < 2 holds
for a being Element of E ex y, z being F -membered Element of E st Ext_eval (p,a) = y + (a * z)
let E be FieldExtension of F; :: thesis: for p being Polynomial of F st deg p < 2 holds
for a being Element of E ex y, z being F -membered Element of E st Ext_eval (p,a) = y + (a * z)
let p be Polynomial of F; :: thesis: ( deg p < 2 implies for a being Element of E ex y, z being F -membered Element of E st Ext_eval (p,a) = y + (a * z) )
assume A: deg p < 2 ; :: thesis: for a being Element of E ex y, z being F -membered Element of E st Ext_eval (p,a) = y + (a * z)
let a be Element of E; :: thesis: ex y, z being F -membered Element of E st Ext_eval (p,a) = y + (a * z)
reconsider q = p as Polynomial of E by FIELD_4:8;
B: ( p is Element of the carrier of (Polynom-Ring F) & q is Element of the carrier of (Polynom-Ring E) ) by POLYNOM3:def 10;
then C: deg q = deg p by FIELD_4:20;
consider yF, zF being Element of F such that
D: p = <%yF,zF%> by A, deg2;
consider y, z being Element of E such that
E: q = <%y,z%> by A, C, deg2;
y = q . 0 by E, POLYNOM5:38
.= yF by D, POLYNOM5:38 ;
then G1: y is F -membered by FIELD_7:def 5;
z = q . 1 by E, POLYNOM5:38
.= zF by D, POLYNOM5:38 ;
then G2: z is F -membered by FIELD_7:def 5;
Ext_eval (p,a) = eval (q,a) by B, FIELD_4:26
.= y + (z * a) by E, POLYNOM5:44
.= y + (a * z) by GROUP_1:def 12 ;
hence ex y, z being F -membered Element of E st Ext_eval (p,a) = y + (a * z) by G1, G2; :: thesis: verum