for L being Field
for f being Polynomial of L st 0 <= deg f holds
( Roots f is finite set & ex m, n being Element of NAT st
( n = deg f & m = card (Roots f) & m <= n ) )