:: deftheorem defines deg1Poly ALGGEO_1:def 3 :
for n being non empty Ordinal
for R being domRing
for a being Function of n,R
for i being Element of n holds deg1Poly (a,i) = (1_1 (i,R)) - ((a . i) | (n,R));