:: deftheorem defines sum_of_coefficients HILB10_5:def 2 :
for n being Ordinal
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds sum_of_coefficients p = Sum (p * (SgmX ((BagOrder n),(Support p))));