:: deftheorem defines constant RATFUNC1:def 2 :
for L being non empty ZeroStr
for p being Polynomial of L holds
( p is constant iff deg p <= 0 );