set a = the non zero Element of F;
H: F is Subfield of E by FIELD_4:7;
then the carrier of F c= the carrier of E by EC_PF_1:def 1;
then reconsider b = the non zero Element of F as Element of E ;
0. F = 0. E by H, EC_PF_1:def 1;
then reconsider b = b as non zero Element of E by STRUCT_0:def 12;
A: X- the non zero Element of F = X- b by FIELD_4:21;
Ext_eval ((X- the non zero Element of F),b) = eval ((X- b),b) by FIELD_4:21, FIELD_4:26
.= b - b by HURWITZ:29
.= 0. E by RLVECT_1:15 ;
then reconsider b = b as F -algebraic Element of E by FIELD_6:43;
MinPoly (b,F) is separable by A, FIELD_6:54;
hence ex b₁ being Element of E st
( not b₁ is zero & b₁ is F -separable ) by defsep; :: thesis: verum