let R be domRing; :: thesis: for p being non zero Polynomial of R holds card (Roots p) <= deg p

let p be non zero Polynomial of R; :: thesis: card (Roots p) <= deg p

ex n being natural number st

( n = card (Roots p) & n <= deg p ) by degpol;

hence card (Roots p) <= deg p ; :: thesis: verum

let p be non zero Polynomial of R; :: thesis: card (Roots p) <= deg p

ex n being natural number st

( n = card (Roots p) & n <= deg p ) by degpol;

hence card (Roots p) <= deg p ; :: thesis: verum