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

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