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