reconsider E = F as FieldExtension of F by FIELD_4:6;
deg (E,F) = 1 by FIELD_7:8;
then A: VecSp (E,F) is finite-dimensional by FIELD_4:def 7;
then E is F -finite by FIELD_4:def 8;
then reconsider E = E as F -algebraic FieldExtension of F ;
take E ; :: thesis: ( E is F -finite & E is F -separable )

now :: thesis: for a being Element of E holds a is F -separable

let a be Element of E; :: thesis: a is F -separable
MinPoly (a,F) = X- a by FIELD_6:54;
hence a is F -separable ; :: thesis: verum

end;

hence ( E is F -finite & E is F -separable ) by A, FIELD_4:def 8; :: thesis: verum