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

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