let L be Field; :: thesis: for p being Element of (Polynom-Ring L)
for q being non zero Element of (Polynom-Ring L) ex u, r being Element of (Polynom-Ring L) st
( p = (u * q) + r & ( r = 0. (Polynom-Ring L) or (deg* L) . r < (deg* L) . q ) )
let p be Element of (Polynom-Ring L); :: thesis: for q being non zero Element of (Polynom-Ring L) ex u, r being Element of (Polynom-Ring L) st
( p = (u * q) + r & ( r = 0. (Polynom-Ring L) or (deg* L) . r < (deg* L) . q ) )
let q be non zero Element of (Polynom-Ring L); :: thesis: ex u, r being Element of (Polynom-Ring L) st
( p = (u * q) + r & ( r = 0. (Polynom-Ring L) or (deg* L) . r < (deg* L) . q ) )
q <> 0. (Polynom-Ring L) ;
then AS: q <> 0_. L by POLYNOM3:def 10;
then reconsider q1 = q as non zero Polynomial of L by UPROOTS:def 5, POLYNOM3:def 10;
reconsider p1 = p as Polynomial of L by POLYNOM3:def 10;
set u = p1 div q1;
set r = p1 mod q1;
reconsider u = p1 div q1, r = p1 mod q1 as Element of (Polynom-Ring L) by POLYNOM3:def 10;
take u ; :: thesis: ex r being Element of (Polynom-Ring L) st
( p = (u * q) + r & ( r = 0. (Polynom-Ring L) or (deg* L) . r < (deg* L) . q ) )
take r ; :: thesis: ( p = (u * q) + r & ( r = 0. (Polynom-Ring L) or (deg* L) . r < (deg* L) . q ) )
A: ((p1 div q1) *' q1) + (p1 mod q1) = ((p1 div q1) *' q1) + (p1 - ((p1 div q1) *' q1)) by HURWITZ:def 6
.= ((p1 div q1) *' q1) + (p1 + (- ((p1 div q1) *' q1))) by POLYNOM3:def 6
.= (((p1 div q1) *' q1) + (- ((p1 div q1) *' q1))) + p1 by POLYNOM3:26
.= (((p1 div q1) *' q1) - ((p1 div q1) *' q1)) + p1 by POLYNOM3:def 6
.= (0_. L) + p1 by POLYNOM3:29
.= p1 by POLYNOM3:28 ;
(p1 div q1) *' q1 = u * q by POLYNOM3:def 10;
hence p = (u * q) + r by A, POLYNOM3:def 10; :: thesis: ( r = 0. (Polynom-Ring L) or (deg* L) . r < (deg* L) . q )

now :: thesis: ( r <> 0. (Polynom-Ring L) implies (deg* L) . r < (deg* L) . q )

assume r <> 0. (Polynom-Ring L) ; :: thesis: (deg* L) . r < (deg* L) . q
then C: p1 mod q1 <> 0_. L by POLYNOM3:def 10;
B: (deg* L) . r = deg* (p1 mod q1) by T
.= deg (p1 mod q1) by C, S ;
(deg* L) . q = deg* q1 by T
.= deg q1 by AS, S ;
hence (deg* L) . r < (deg* L) . q by B, degA; :: thesis: verum

end;

hence ( r = 0. (Polynom-Ring L) or (deg* L) . r < (deg* L) . q ) ; :: thesis: verum