let p be irreducible Element of the carrier of (Polynom-Ring F); :: thesis: p is separable
A: (Deriv F) . p <> 0_. F by FIELD_14:69;

now :: thesis: for E being SplittingField of p
for a being Element of E st a is_a_root_of p,E holds
multiplicity (p,a) = 1

let E be SplittingField of p; :: thesis: for a being Element of E st a is_a_root_of p,E holds
multiplicity (p,a) = 1
let a be Element of E; :: thesis: ( a is_a_root_of p,E implies multiplicity (p,a) = 1 )
the carrier of (Polynom-Ring F) c= the carrier of (Polynom-Ring E) by FIELD_4:10;
then reconsider p1 = p as Element of the carrier of (Polynom-Ring E) ;
deg p1 = deg p by FIELD_4:20;
then reconsider p1 = p1 as non zero Element of the carrier of (Polynom-Ring E) by RING_4:def 4, RATFUNC1:def 2;
B: p splits_in E by FIELD_8:def 1;
assume a is_a_root_of p,E ; :: thesis: multiplicity (p,a) = 1
then 0. E = Ext_eval (p,a) by FIELD_4:def 2
.= eval (p1,a) by FIELD_4:26 ;
then multiplicity (p1,a) >= 1 by UPROOTS:52, POLYNOM5:def 7;
then C: multiplicity (p,a) >= 1 by FIELD_14:def 6;
multiplicity (p,a) <= 1 by A, B, lemsep1;
hence multiplicity (p,a) = 1 by C, XXREAL_0:1; :: thesis: verum

end;

hence p is separable ; :: thesis: verum