theorem Th44: :: NIVEN:46

for L being non degenerated right_complementable add-associative right_zeroed well-unital distributive associative domRing-like doubleLoopStr
for p, q being Polynomial of L holds LC (p *' q) = (LC p) * (LC q)