theorem Th7: :: BASEL_2:7

for n being Nat
for L being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for z being Element of L
for p being Polynomial of L holds (p *' <%z%>) . n = (p . n) * z