theorem Th23: :: UPROOTS:26

for L being non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr
for p, q, r being Polynomial of L holds (p *' q) - (p *' r) = p *' (q - r)