set a = the Element of F;
reconsider p = (X- the Element of F) `^ 2 as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
deg ((X- the Element of F) `^ 2) = 2 by Lm12a;
then reconsider p = p as monic non constant Element of the carrier of (Polynom-Ring F) by RING_4:def 4;
take p ; :: thesis: p is inseparable
set E = the SplittingField of p;
F is Subfield of the SplittingField of p by FIELD_4:7;
then the carrier of F c= the carrier of the SplittingField of p by EC_PF_1:def 1;
then reconsider b = the Element of F as Element of the SplittingField of p ;
reconsider q = (X- b) `^ 2 as Element of the carrier of (Polynom-Ring the SplittingField of p) by POLYNOM3:def 10;
2 = multiplicity (((X- b) `^ 2),b) by ro0
.= multiplicity (((X- the Element of F) `^ 2),b) by XYZ, FIELD_14:def 6 ;
hence p is inseparable by ThSep01; :: thesis: verum