:: deftheorem T defines deg* RING_2:def 17 :
for L being Field
for b₂ being Function of (Polynom-Ring L),NAT holds
( b₂ = deg* L iff for p being Polynomial of L holds b₂ . p = deg* p );