for R being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ex P being Function of R,(Polynom-Ring (0,R)) st P is RingIsomorphism