take a = 1. E; :: thesis: ( not a is zero & a is F -algebraic )
A: F is Subring of E by FIELD_4:def 1;
then a = 1. F by C0SP1:def 3;
then In (a,E) is_integral_over F by A, ALGNUM_1:23;
hence ( not a is zero & a is F -algebraic ) by FIELD_6:42; :: thesis: verum