for L being non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr
for p1, p2 being Polynomial of L holds
( - (p1 *' p2) = (- p1) *' p2 & - (p1 *' p2) = p1 *' (- p2) )