let R be domRing; :: thesis: for S being non empty finite Subset of R
for p being Ppoly of R,S holds deg p = card S
let S be non empty finite Subset of R; :: thesis: for p being Ppoly of R,S holds deg p = card S
let p be Ppoly of R,S; :: thesis: deg p = card S
thus deg p = card (Bag S) by dpp
.= card S by UPROOTS:13 ; :: thesis: verum