theorem Th25: :: UPROOTS:28

for L being non empty right_complementable distributive Abelian add-associative right_zeroed domRing-like doubleLoopStr
for p, q, r being Polynomial of L st p <> 0_. L & p *' q = p *' r holds
q = r