theorem Th12: :: BASEL_2:12

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)