for k, n being Nat
for L being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for a being Polynomial of L holds (n * a) . k = n * (a . k)