:: deftheorem Def9 defines DegreeFunction INT_3:def 9 :
for E being non empty Euclidian doubleLoopStr
for b₂ being Function of E,NAT holds
( b₂ is DegreeFunction of E iff for a, b being Element of E st b <> 0. E holds
ex q, r being Element of E st
( a = (q * b) + r & ( r = 0. E or b₂ . r < b₂ . b ) ) );