let F be Field; :: thesis: for p being non constant separable Element of the carrier of (Polynom-Ring F) holds
( deg p = card (Roots p) iff p splits_in F )
let p be non constant separable Element of the carrier of (Polynom-Ring F); :: thesis: ( deg p = card (Roots p) iff p splits_in F )
deg p > 0 by RING_4:def 4;
then K: p is non constant Polynomial of F by RATFUNC1:def 2;
reconsider E = F as FieldExtension of F by FIELD_4:6;
reconsider pE = p as non constant Element of the carrier of (Polynom-Ring E) ;

now :: thesis: ( p splits_in F implies deg p = card (Roots p) )

assume B: p splits_in F ; :: thesis: deg p = card (Roots p)
then consider c being non zero Element of F, q being Ppoly of F such that
C: p = c * q by FIELD_4:def 5;
reconsider qE = q as Element of the carrier of (Polynom-Ring E) by POLYNOM3:def 10;
H1: c * q = (@ (c,E)) * qE by FIELD_7:def 4;

now :: thesis: for a being Element of F st a is_a_root_of q holds
1 = multiplicity (q,a)

let a be Element of F; :: thesis: ( a is_a_root_of q implies 1 = multiplicity (q,a) )
assume a is_a_root_of q ; :: thesis: 1 = multiplicity (q,a)
then C3: eval (qE,(@ (a,E))) = 0. E by FIELD_7:def 4;
Ext_eval (p,(@ (a,E))) = eval (pE,(@ (a,E))) by FIELD_4:26
.= (@ (c,E)) * (eval (qE,(@ (a,E)))) by C, H1, POLYNOM5:30
.= 0. E by C3 ;
hence 1 = multiplicity (p,(@ (a,E))) by B, ThSep0, FIELD_4:def 2
.= multiplicity (p,a) by multi3
.= multiplicity (q,a) by C, lems ;
:: thesis: verum

end;

then D: q is Ppoly of F,(Roots q) by FIELD_14:30;
thus deg p = deg q by C, RING_5:4
.= card (Roots q) by D, RING_5:60
.= card (Roots p) by C, RING_5:19 ; :: thesis: verum

end;

hence ( deg p = card (Roots p) iff p splits_in F ) by K, ThsepsplA; :: thesis: verum