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