:: deftheorem defines Coeff FIELD_7:def 3 :
for F being Field
for p being Polynomial of F holds Coeff p = { (p . i) where i is Element of NAT : p . i <> 0. F } ;