:: deftheorem S defines deg* RING_2:def 16 :
for L being Field
for p being Polynomial of L holds
( ( p <> 0_. L implies deg* p = deg p ) & ( not p <> 0_. L implies deg* p = 0 ) );