let F be Field; :: thesis: for p being Polynomial of F
for q being non zero Polynomial of F holds deg (p mod q) < deg q
let p be Polynomial of F; :: thesis: for q being non zero Polynomial of F holds deg (p mod q) < deg q
let q be non zero Polynomial of F; :: thesis: deg (p mod q) < deg q
q <> 0_. F ;
then consider t being Polynomial of F such that
C: ( p = ((p div q) *' q) + t & deg t < deg q ) by HURWITZ:def 5;
p mod q = (((p div q) *' q) + t) - ((p div q) *' q) by C, HURWITZ:def 6
.= t + (((p div q) *' q) - ((p div q) *' q)) by POLYNOM3:26
.= t + (0_. F) by POLYNOM3:29 ;
hence deg (p mod q) < deg q by C; :: thesis: verum