let F be Field; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F) holds
( p is separable iff ex E being FieldExtension of F st card (Roots (E,p)) = deg p )
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: ( p is separable iff ex E being FieldExtension of F st card (Roots (E,p)) = deg p )

A: now :: thesis: ( p is separable implies ex E being FieldExtension of F st card (Roots (E,p)) = deg p )

assume AS: p is separable ; :: thesis: ex E being FieldExtension of F st card (Roots (E,p)) = deg p
set K = the SplittingField of p;
the carrier of (Polynom-Ring F) c= the carrier of (Polynom-Ring the SplittingField of p) by FIELD_4:10;
then reconsider q = p as Element of the carrier of (Polynom-Ring the SplittingField of p) ;
( deg p > 0 & deg p = deg q ) by RING_4:def 4, FIELD_4:20;
then reconsider q = q as non constant Element of the carrier of (Polynom-Ring the SplittingField of p) by RING_4:def 4;
p splits_in the SplittingField of p by FIELD_8:def 1;
then consider c being non zero Element of the SplittingField of p, r being Ppoly of the SplittingField of p such that
H: p = c * r by FIELD_4:def 5;

now :: thesis: not q is inseparable

assume q is inseparable ; :: thesis: contradiction
then consider E being FieldExtension of the SplittingField of p such that
B: not for a being Element of E holds multiplicity (q,a) <= 1 by ThSep02;
consider a being Element of E such that
C: multiplicity (q,a) > 1 by B;
reconsider E = E as the SplittingField of p -extending FieldExtension of F ;
reconsider a = a as Element of E ;
multiplicity (q,a) = multiplicity (p,a) by sepsep;
hence contradiction by C, AS, ThSep02; :: thesis: verum

end;

then D: card (Roots q) = deg q by H, FIELD_4:def 5, Thsepspl
.= deg p by FIELD_4:20 ;
Roots q = Roots ( the SplittingField of p,p) by FIELD_7:13;
hence ex E being FieldExtension of F st card (Roots (E,p)) = deg p by D; :: thesis: verum

end;

now :: thesis: ( ex E being FieldExtension of F st card (Roots (E,p)) = deg p implies p is separable )

assume ex E being FieldExtension of F st card (Roots (E,p)) = deg p ; :: thesis: p is separable
then consider E being FieldExtension of F such that
AS: card (Roots (E,p)) = deg p ;
the carrier of (Polynom-Ring F) c= the carrier of (Polynom-Ring E) by FIELD_4:10;
then reconsider q = p as Element of the carrier of (Polynom-Ring E) ;
reconsider q = q as Polynomial of E ;
( deg p > 0 & deg p = deg q ) by RING_4:def 4, FIELD_4:20;
then reconsider q = q as non constant Polynomial of E by RATFUNC1:def 2;
A: card (Roots q) = card (Roots (E,p)) by FIELD_7:13
.= deg q by AS, FIELD_4:20 ;
consider c being non zero Element of E, r being Ppoly of E such that
H: q = c * r by FIELD_4:def 5, A, ThsepsplA;

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

let a be Element of E; :: thesis: multiplicity (p,a) <= 1
multiplicity (q,a) = multiplicity (p,a) by FIELD_14:def 6;
hence multiplicity (p,a) <= 1 by A, ThsepsplA; :: thesis: verum

end;

hence p is separable by H, FIELD_4:def 5, ThSep03; :: thesis: verum

end;

hence ( p is separable iff ex E being FieldExtension of F st card (Roots (E,p)) = deg p ) by A; :: thesis: verum