:: deftheorem Def1 defines Coeff HURWITZ:def 1 :
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for F being FinSequence of (Polynom-Ring L)
for i being Element of NAT
for b₄ being FinSequence of L holds
( b₄ = Coeff (F,i) iff ( len b₄ = len F & ( for j being Element of NAT st j in dom b₄ holds
ex p being Polynomial of L st
( p = F . j & b₄ . j = p . i ) ) ) );