theorem ABC: :: FIELD_15:67

for F being Field
for p being non zero Polynomial of F holds
( card (Roots p) < card (BRoots p) iff ex a being Element of F st multiplicity (p,a) > 1 )