theorem Th18: :: RATFUNC1:18

for L being non empty right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for p being Polynomial of L
for a being Element of L holds LC (a * p) = a * (LC p)