let R be domRing; :: thesis: for B being non zero bag of the carrier of R
for p being Ppoly of R,B holds deg p = card (BRoots p)
let B be non zero bag of the carrier of R; :: thesis: for p being Ppoly of R,B holds deg p = card (BRoots p)
let p be Ppoly of R,B; :: thesis: deg p = card (BRoots p)
thus card (BRoots p) = card B by pf2
.= deg p by dpp ; :: thesis: verum