:: deftheorem Def1 defines rpoly NUMBER19:def 1 :
for L being non empty right_complementable add-associative right_zeroed distributive unital doubleLoopStr
for z being FinSequence of the carrier of L
for f being NAT -valued FinSequence
for b₄ being FinSequence of the carrier of (Polynom-Ring L) holds
( b₄ = rpoly (f,z) iff ( len b₄ = len f & ( for i being Nat st 1 <= i & i <= len f holds
b₄ . i = rpoly ((f /. i),(z /. i)) ) ) );