theorem ThsepsplA: :: FIELD_15:69

for F being Field
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 ) ) )