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

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