let F be Field; :: thesis: for p, q being Polynomial of F holds p = ((p div q) *' q) + (p mod q)
let p, q be Polynomial of F; :: thesis: p = ((p div q) *' q) + (p mod q)
thus p = p + (0_. F) by POLYNOM3:28
.= p + (((p div q) *' q) - ((p div q) *' q)) by POLYNOM3:29
.= (p + (- ((p div q) *' q))) + ((p div q) *' q) by POLYNOM3:26
.= ((p div q) *' q) + (p mod q) ; :: thesis: verum