let L be Field; :: thesis: ex f being Function of (Polynom-Ring L),NAT st
for p, q being Element of (Polynom-Ring L) st q <> 0. (Polynom-Ring L) holds
ex u, r being Element of (Polynom-Ring L) st
( p = (u * q) + r & ( r = 0. (Polynom-Ring L) or f . r < f . q ) )
take f = deg* L; :: thesis: for p, q being Element of (Polynom-Ring L) st q <> 0. (Polynom-Ring L) holds
ex u, r being Element of (Polynom-Ring L) st
( p = (u * q) + r & ( r = 0. (Polynom-Ring L) or f . r < f . q ) )

now :: thesis: for p, q being Element of (Polynom-Ring L) st q <> 0. (Polynom-Ring L) holds
ex u, r being Element of (Polynom-Ring L) st
( p = (u * q) + r & ( r = 0. (Polynom-Ring L) or f . r < f . q ) )

let p, q be Element of (Polynom-Ring L); :: thesis: ( q <> 0. (Polynom-Ring L) implies ex u, r being Element of (Polynom-Ring L) st
( p = (u * q) + r & ( r = 0. (Polynom-Ring L) or f . r < f . q ) ) )
assume q <> 0. (Polynom-Ring L) ; :: thesis: ex u, r being Element of (Polynom-Ring L) st
( p = (u * q) + r & ( r = 0. (Polynom-Ring L) or f . r < f . q ) )
then not q is zero ;
hence ex u, r being Element of (Polynom-Ring L) st
( p = (u * q) + r & ( r = 0. (Polynom-Ring L) or f . r < f . q ) ) by thEucl1; :: thesis: verum

end;

hence for p, q being Element of (Polynom-Ring L) st q <> 0. (Polynom-Ring L) holds
ex u, r being Element of (Polynom-Ring L) st
( p = (u * q) + r & ( r = 0. (Polynom-Ring L) or f . r < f . q ) ) ; :: thesis: verum