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