let a be F -algebraic Element of E; :: thesis: a is K -algebraic
consider p being non zero Polynomial of F such that
A: Ext_eval (p,a) = 0. E by FIELD_6:43;
reconsider p = p as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
the carrier of (Polynom-Ring F) c= the carrier of (Polynom-Ring K) by FIELD_4:10;
then reconsider p1 = p as Element of the carrier of (Polynom-Ring K) ;
p <> 0_. F ;
then p1 <> 0_. K by FIELD_4:12;
then reconsider p1 = p1 as non zero Element of the carrier of (Polynom-Ring K) by UPROOTS:def 5;
Ext_eval (p1,a) = 0. E by A, FIELD_7:15;
hence a is K -algebraic by FIELD_6:43; :: thesis: verum