for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr holds Polynom-Ring ({},L) is_ringisomorph_to L