let F be Field; :: thesis: for p being non constant Polynomial of F holds
( deg p = card (Roots p) iff ( p splits_in F & ( for a being Element of F holds multiplicity (p,a) <= 1 ) ) )
let p be non constant Polynomial of F; :: thesis: ( deg p = card (Roots p) iff ( p splits_in F & ( for a being Element of F holds multiplicity (p,a) <= 1 ) ) )

A: now :: thesis: ( deg p = card (Roots p) implies ( p splits_in F & ( for a being Element of F holds multiplicity (p,a) <= 1 ) ) )

assume AS: deg p = card (Roots p) ; :: thesis: ( p splits_in F & ( for a being Element of F holds multiplicity (p,a) <= 1 ) )
H: card (BRoots p) <= deg p by RING_5:42;
deg p <= card (BRoots p) by AS, RING_5:65;
then consider c being Element of F, q being Ppoly of F such that
A: p = c * q by H, XXREAL_0:1, RING_5:66;
p <> 0_. F ;
then not c is zero by A, POLYNOM5:26;
hence ( p splits_in F & ( for a being Element of F holds multiplicity (p,a) <= 1 ) ) by AS, A, H, ABC, FIELD_4:def 5; :: thesis: verum

end;

now :: thesis: ( p splits_in F & ( for a being Element of F holds multiplicity (p,a) <= 1 ) implies deg p = card (Roots p) )

assume AS: ( p splits_in F & ( for a being Element of F holds multiplicity (p,a) <= 1 ) ) ; :: thesis: deg p = card (Roots p)
set Np = NormPolynomial p;
( deg p > 0 & deg p = (len p) - 1 ) by RATFUNC1:def 2, HURWITZ:def 2;
then V: len p <> 0 ;
U: p is non zero Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
then W: ( NormPolynomial p = ((LC p) ") * p & LC p <> 0. F ) by RING_4:23;
then (LC p) * (NormPolynomial p) = ((LC p) * ((LC p) ")) * p by RING_4:11
.= (1. F) * p by W, VECTSP_1:def 10
.= p ;
then consider c being non zero Element of F, q being Ppoly of F such that
A: NormPolynomial p = c * q by AS, FIELD_8:9, FIELD_4:def 5;
c = c * (1. F)
.= c * (LC q) by RATFUNC1:def 7
.= LC (c * q) by RING_5:5
.= 1. F by A, RATFUNC1:def 7 ;
then reconsider Np = NormPolynomial p as Ppoly of F by A;
B: Roots Np = Roots p by V, POLYNOM5:61;

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

let a be Element of F; :: thesis: ( a is_a_root_of Np implies multiplicity (Np,a) = 1 )
assume a is_a_root_of Np ; :: thesis: multiplicity (Np,a) = 1
then a is_a_root_of p by V, POLYNOM5:59;
then ( multiplicity (p,a) >= 1 & multiplicity (p,a) <= 1 ) by AS, UPROOTS:52;
then multiplicity (p,a) = 1 by XXREAL_0:1;
hence multiplicity (Np,a) = 1 by ThsepsplB; :: thesis: verum

end;

then C: Np is Ppoly of F,(Roots Np) by FIELD_14:30;
thus deg p = deg Np by U, REALALG3:11
.= card (Roots p) by B, C, RING_5:60 ; :: thesis: verum

end;

hence ( deg p = card (Roots p) iff ( p splits_in F & ( for a being Element of F holds multiplicity (p,a) <= 1 ) ) ) by A; :: thesis: verum