set a = the Element of F;
take p = X- the Element of F; :: thesis: p is separable
set K = the SplittingField of p;
A: (Deriv F) . (X- the Element of F) = 1_. F by FIELD_14:61;
p splits_in the SplittingField of p by FIELD_8:def 1;
then for a being Element of the SplittingField of p holds multiplicity (p,a) <= 1 by A, lemsep1;
hence p is separable by ThSep01; :: thesis: verum