for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for p, q being Polynomial of L st p - q = 0_. L holds
p = q