for L being Field
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 ) )