let F be Field; :: thesis: for p, q being Polynomial of F st deg p < deg q holds
p mod q = p
let p, q be Polynomial of F; :: thesis: ( deg p < deg q implies p mod q = p )
assume A1: deg p < deg q ; :: thesis: p mod q = p
0_. F = 0. (Polynom-Ring F) by POLYNOM3:def 10;
then H: - (0_. F) = - (0. (Polynom-Ring F)) by lm
.= 0. (Polynom-Ring F) ;

A0: now :: thesis: not q = 0_. F

assume A0: q = 0_. F ; :: thesis: contradiction
then deg p < - 1 by A1, HURWITZ:20;
hence contradiction by A0, A1, T8b; :: thesis: verum

end;

p = (0_. F) + p by POLYNOM3:28
.= ((0_. F) *' q) + p by POLYNOM3:34 ;
hence p mod q = p - ((0_. F) *' q) by A0, A1, HURWITZ:def 5
.= p - (0_. F) by POLYNOM3:34
.= p + (0_. F) by H, POLYNOM3:def 10
.= p by POLYNOM3:28 ;
:: thesis: verum