now :: thesis: for a being Element of (F_Alg E) holds a is F -algebraic

let a be Element of (F_Alg E); :: thesis: a is F -algebraic
the carrier of (F_Alg E) = Alg_El E by d
.= { x where x is F -algebraic Element of E : verum } ;
then a in { x where x is F -algebraic Element of E : verum } ;
then consider a1 being F -algebraic Element of E such that
A: a1 = a ;
consider p being non zero Polynomial of F such that
B: Ext_eval (p,a1) = 0. E by FIELD_6:43;
reconsider p = p as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
E is F_Alg E -extending by ee;
then Ext_eval (p,a) = 0. E by A, B, lemma7a
.= 0. (F_Alg E) by d ;
hence a is F -algebraic by FIELD_6:43; :: thesis: verum

end;

hence F_Alg E is F -algebraic ; :: thesis: verum