F is Subring of E by FIELD_4:def 1;
then In (a,E) is_integral_over F by ALGNUM_1:23;
hence @ (a,E) is F -algebraic by FIELD_6:42; :: thesis: verum