ex f being Function of (Polynom-Ring L),NAT st
for a, b being Element of (Polynom-Ring L) st b <> 0. (Polynom-Ring L) holds
ex q, r being Element of (Polynom-Ring L) st
( a = (q * b) + r & ( r = 0. (Polynom-Ring L) or f . r < f . b ) ) by thEucl2;
hence Polynom-Ring L is Euclidian by INT_3:def 8; :: thesis: verum