let F be Field; :: thesis: for E being FieldExtension of F
for a being F -algebraic Element of E
for b being Element of E holds
( b in the carrier of (FAdj (F,{a})) iff ex p being Polynomial of F st
( deg p < deg (MinPoly (a,F)) & b = Ext_eval (p,a) ) )
let E be FieldExtension of F; :: thesis: for a being F -algebraic Element of E
for b being Element of E holds
( b in the carrier of (FAdj (F,{a})) iff ex p being Polynomial of F st
( deg p < deg (MinPoly (a,F)) & b = Ext_eval (p,a) ) )
let a be F -algebraic Element of E; :: thesis: for b being Element of E holds
( b in the carrier of (FAdj (F,{a})) iff ex p being Polynomial of F st
( deg p < deg (MinPoly (a,F)) & b = Ext_eval (p,a) ) )
let b be Element of E; :: thesis: ( b in the carrier of (FAdj (F,{a})) iff ex p being Polynomial of F st
( deg p < deg (MinPoly (a,F)) & b = Ext_eval (p,a) ) )
H: E is Polynom-Ring F -homomorphic ;

A: now :: thesis: ( ex p being Polynomial of F st
( deg p < deg (MinPoly (a,F)) & b = Ext_eval (p,a) ) implies b in the carrier of (FAdj (F,{a})) )

assume ex p being Polynomial of F st
( deg p < deg (MinPoly (a,F)) & b = Ext_eval (p,a) ) ; :: thesis: b in the carrier of (FAdj (F,{a}))
then b in { (Ext_eval (p,a)) where p is Polynomial of F : verum } ;
then b in the carrier of (RAdj (F,{a})) by H, FIELD_6:45;
hence b in the carrier of (FAdj (F,{a})) by H, FIELD_6:56; :: thesis: verum

end;

now :: thesis: ( b in the carrier of (FAdj (F,{a})) implies ex p being Polynomial of F st
( deg p < deg (MinPoly (a,F)) & b = Ext_eval (p,a) ) )

assume b in the carrier of (FAdj (F,{a})) ; :: thesis: ex p being Polynomial of F st
( deg p < deg (MinPoly (a,F)) & b = Ext_eval (p,a) )
then b in the carrier of (RAdj (F,{a})) by H, FIELD_6:56;
then b in { (Ext_eval (p,a)) where p is Polynomial of F : verum } by H, FIELD_6:45;
then consider q being Polynomial of F such that
E: b = Ext_eval (q,a) ;
set ma = MinPoly (a,F);
set r = q mod (MinPoly (a,F));
B: F is Subring of E by FIELD_4:def 1;
C: q = ((q div (MinPoly (a,F))) *' (MinPoly (a,F))) + (q mod (MinPoly (a,F))) by RING_4:4;
D: deg (q mod (MinPoly (a,F))) < deg (MinPoly (a,F)) by FIELD_5:16;
Ext_eval (q,a) = (Ext_eval (((q div (MinPoly (a,F))) *' (MinPoly (a,F))),a)) + (Ext_eval ((q mod (MinPoly (a,F))),a)) by C, B, ALGNUM_1:15
.= ((Ext_eval ((q div (MinPoly (a,F))),a)) * (Ext_eval ((MinPoly (a,F)),a))) + (Ext_eval ((q mod (MinPoly (a,F))),a)) by B, ALGNUM_1:20
.= ((Ext_eval ((q div (MinPoly (a,F))),a)) * (0. E)) + (Ext_eval ((q mod (MinPoly (a,F))),a)) by FIELD_6:52
.= Ext_eval ((q mod (MinPoly (a,F))),a) ;
hence ex p being Polynomial of F st
( deg p < deg (MinPoly (a,F)) & b = Ext_eval (p,a) ) by D, E; :: thesis: verum

end;

hence ( b in the carrier of (FAdj (F,{a})) iff ex p being Polynomial of F st
( deg p < deg (MinPoly (a,F)) & b = Ext_eval (p,a) ) ) by A; :: thesis: verum