for L being non empty right_complementable left-distributive add-associative right_zeroed doubleLoopStr
for a, b being Element of L
for p being Polynomial of L holds
( (<%a,b%> *' p) . 0 = a * (p . 0) & ( for i being Nat holds (<%a,b%> *' p) . (i + 1) = (a * (p . (i + 1))) + (b * (p . i)) ) )