set a = 1. F;
F is Subring of E by FIELD_4:def 1;
then In ((1. F),E) is_integral_over F by ALGNUM_1:23;
hence ex b₁ being Element of E st b₁ is F -algebraic by alg1; :: thesis: verum